Regularity in the distinguished variable: the elementary reading

IsRegularIn g d says that the image of splitFirst K m g in the residue field of the tail ring MvPowerSeries (Fin m) K has order d. The k-th coefficient of that image is the residue of the coefficient series of x_0^k, which vanishes iff that series has zero constant term, i.e. iff the pure x_0-coefficient of g at x_0^k vanishes. So g is regular of order d iff its pure x_0-coefficients vanish below degree d and not at degree d, that is, g(x_0, 0, …, 0) = x_0^d e(x_0) with e(0) ≠ 0: the printed f_a(0, …, 0, x_m) ∼ x_m^e of [BM88, proof of Theorem 4.4, p. 24]. In particular the residue image is nonzero, which is the hypothesis of Mathlib's Weierstrass theorems. The module ends with the remark that a factorization f = u · P with u nowhere zero on a polydisc gives f and P the same zero set there, the printed item (3) of the same proof.

The coefficient field K is ℝ or ℂ ([RCLike K]).

theorem Analytic.residue_eq_zero_iff {K : Type u_1} [RCLike K] {m : ℕ} (a : MvPowerSeries (Fin m) K) : (IsLocalRing.residue (MvPowerSeries (Fin m) K)) a = 0 ↔ MvPowerSeries.constantCoeff a = 0

The residue of a series in the tail variables vanishes iff its constant coefficient does.

theorem Analytic.constantCoeff_coeff_splitFirst {K : Type u_1} [RCLike K] {m : ℕ} (g : MvPowerSeries (Fin (m + 1)) K) (k : ℕ) : MvPowerSeries.constantCoeff ((PowerSeries.coeff k) ((splitFirst K m) g)) = (MvPowerSeries.coeff (Finsupp.single 0 k)) g

The constant coefficient of the k-th x_0-coefficient series is the pure x_0-coefficient of g at x_0^k.

theorem Analytic.isRegularIn_iff {K : Type u_1} [RCLike K] {m : ℕ} (g : MvPowerSeries (Fin (m + 1)) K) (d : ℕ) : IsRegularIn g d ↔ (∀ k < d, (MvPowerSeries.coeff (Finsupp.single 0 k)) g = 0) ∧ (MvPowerSeries.coeff (Finsupp.single 0 d)) g ≠ 0

The elementary reading of regularity: the pure x_0-coefficients of g vanish below degree d and not at degree d.

theorem Analytic.map_residue_ne_zero_of_isRegularIn {K : Type u_1} [RCLike K] {m : ℕ} {g : MvPowerSeries (Fin (m + 1)) K} {d : ℕ} (hg : IsRegularIn g d) : (PowerSeries.map (IsLocalRing.residue (MvPowerSeries (Fin m) K))) ((splitFirst K m) g) ≠ 0

Regularity gives Mathlib's Weierstrass hypothesis g.map (IsLocalRing.residue A) ≠ 0.

theorem Analytic.zero_iff_of_unit_mul {K : Type u_1} [RCLike K] {m : ℕ} {ρ : Radius (m + 1)} {f u P : (Fin (m + 1) → K) → K} (hu : ∀ x ∈ polydisc K ρ, u x ≠ 0) (hfP : ∀ x ∈ polydisc K ρ, f x = u x * P x) (x : Fin (m + 1) → K) : x ∈ polydisc K ρ → (f x = 0 ↔ P x = 0)

Where f = u · P with u nonvanishing, the zero sets of f and P agree: the printed {f = 0} = {f_1 ⋯ f_r g = 0} of [BM88, proof of Theorem 4.4, p. 24, item (3)].