Conv K m is a domain, and its units are the series with nonzero constant term

Conv K m is a subalgebra of MvPowerSeries (Fin m) K, which has no zero divisors, so it is a domain. A convergent series f with a_0 ≠ 0 is a unit of Conv K m: its function is analytic near 0 with nonzero value a_0, so 1 / evalSeries f is analytic near 0 and, by Bridge.lean, is the function of a convergent series c; the function of f c is then 1 near 0 (multiplicativity of evaluation), so f c = 1 by uniqueness of coefficients. Conversely a unit of Conv K m is a unit of the formal power series ring, whose constant term is a unit (MvPowerSeries.isUnit_iff_constantCoeff). Standard [GR71, Kapitel I], where the inverse is constructed through the majorant norms; here it comes from Mathlib's AnalyticAt.inv. These are the basic ring-theoretic facts about the local ring of germs that the Weierstrass theory and the germ theory use throughout.

theorem Analytic.isUnit_iff_constantCoeff_ne_zero {K : Type u_1} [RCLike K] {m : ℕ} {f : MvPowerSeries (Fin m) K} (hf : f ∈ Conv K m) : IsUnit ⟨f, hf⟩ ↔ MvPowerSeries.constantCoeff f ≠ 0

A convergent series is a unit of Conv K m iff its constant coefficient is nonzero.