Unit criterion for noncommutative formal power series
ID: unit-criterion-for-noncommutative-formal-power-series
A noncommutative formal power series over a field is a unit exactly when its constant term is nonzero. Necessity follows because the constant term is a ring homomorphism to the coefficient field. For sufficiency, write with and of zero constant term. The formal geometric series is well-defined because only can contribute to a word of length . Its left and right products with are , by the finite geometric-series identity in each fixed degree. Multiplying by gives the inverse of .
New to topics? Read the docs here!