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

Instance

If R has NoZeroDivisors, then so does MvPowerSeries σ R.

TODO

• 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 [Fields1971]

theorem MvPowerSeries.mem_nonZeroDivisors_of_constantCoeff {σ : Type u_1} {R : Type u_2} [Semiring R] {φ : MvPowerSeries σ R} (hφ : (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

theorem MvPowerSeries.monomial_mem_nonzeroDivisors {σ : Type u_1} {R : Type u_2} [Semiring R] {n : σ →₀ ℕ} {r : R} : (monomial R n) r ∈ nonZeroDivisors (MvPowerSeries σ R) ↔ r ∈ nonZeroDivisors R

theorem MvPowerSeries.X_mem_nonzeroDivisors {σ : Type u_1} {R : Type u_2} [Semiring R] {i : σ} : X i ∈ nonZeroDivisors (MvPowerSeries σ R)

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