Commit 2024-07-16 12:01 88aed88e

feat (Mathlib/RingTheory/MvPowerSeries/NoZeroDivisors) : power series with constant coeff unit is a unit (#14454) Prove properties of the inverse of a power series over a general Ring. We prove that a multivariate power series is a unit iff its constant coefficient is a unit. The proof uses the construction of the inverse (which is a priori only a left inverse) and proves it is a right inverse. To that aim, we prove the more general result that if the constant coefficient of a multivariate power series is not a zero divisor, then the power series itself is not a zero divisor.