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

• MvPowerSeries.order_mul : multiplicativity of MvPowerSeries.order if the semiring R has no zero divisors

Instance

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

TODO

• Transfer/adapt these results to HahnSeries.

Remark

The analogue of Polynomial.notMem_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φ : (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)

theorem MvPowerSeries.weightedOrder_mul {σ : Type u_1} {R : Type u_2} [Semiring R] [NoZeroDivisors R] (w : σ → ℕ) (f g : MvPowerSeries σ R) : weightedOrder w (f * g) = weightedOrder w f + weightedOrder w g

theorem MvPowerSeries.order_mul {σ : Type u_1} {R : Type u_2} [Semiring R] [NoZeroDivisors R] (f g : MvPowerSeries σ R) : (f * g).order = f.order + g.order