ZeroDivisors in a MvPowerSeries ring

• mem_nonZeroDivisors_of_constantCoeff proves that a multivariate power series whose constant coefficient is not a zero divisor is itself not a zero divisor

TODO

• A subsequent PR https://github.com/leanprover-community/mathlib4/pull/14571 proves that if R has no zero divisors, then so does MvPowerSeries σ R.

• Transfer/adapt these results to HahnSeries.

Remark

The analogue of Polynomial.nmem_nonZeroDivisors_iff (McCoy theorem) holds for power series over a noetherian ring, but not in general. See [Fie71]

theorem MvPowerSeries.mem_nonZeroDivisors_of_constantCoeff {σ : Type u_1} {R : Type u_2} [Semiring R] {φ : MvPowerSeries σ R} (hφ : (MvPowerSeries.constantCoeff σ R) φ ∈ nonZeroDivisors R) : φ ∈ nonZeroDivisors (MvPowerSeries σ R)

A multivariate power series is not a zero divisor when its constant coefficient is not a zero divisor

instance MvPowerSeries.instNoZeroDivisors {σ : Type u_3} {R : Type u_4} [Semiring R] [NoZeroDivisors R] : NoZeroDivisors (MvPowerSeries σ R)

Equations

• ⋯ = ⋯