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_nonZeroDivisorsRight_of_constantCoeff {σ : Type u_1} {R : Type u_2} [Semiring R] {φ : MvPowerSeries σ R} (hφ : constantCoeff φ ∈ nonZeroDivisorsRight R) : φ ∈ nonZeroDivisorsRight (MvPowerSeries σ R)

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

theorem MvPowerSeries.mem_nonZeroDivisors_of_constantCoeff {σ : Type u_1} {R : Type u_2} [Semiring R] {φ : MvPowerSeries σ R} (hφ : constantCoeff φ ∈ 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_nonZeroDivisorsLeft {σ : Type u_1} {R : Type u_2} [Semiring R] {n : σ →₀ ℕ} {r : R} : (monomial n) r ∈ nonZeroDivisorsLeft (MvPowerSeries σ R) ↔ r ∈ nonZeroDivisorsLeft R

@[deprecated MvPowerSeries.monomial_mem_nonZeroDivisorsLeft (since := "2026-09-28")]

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

Alias of MvPowerSeries.monomial_mem_nonZeroDivisorsLeft.

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

@[deprecated MvPowerSeries.monomial_mem_nonZeroDivisorsRight (since := "2026-09-28")]

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

Alias of MvPowerSeries.monomial_mem_nonZeroDivisorsRight.

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

@[deprecated MvPowerSeries.monomial_mem_nonZeroDivisors (since := "2026-09-28")]

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

Alias of MvPowerSeries.monomial_mem_nonZeroDivisors.

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

@[deprecated MvPowerSeries.X_mem_nonZeroDivisors (since := "2026-09-28")]

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

Alias of MvPowerSeries.X_mem_nonZeroDivisors.

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.weightedOrder_prod {σ : Type u_1} {R : Type u_3} [CommSemiring R] [NoZeroDivisors R] [Nontrivial R] {ι : Type u_4} (w : σ → ℕ) (f : ι → MvPowerSeries σ R) (s : Finset ι) : weightedOrder w (∏ i ∈ s, f i) = ∑ i ∈ s, weightedOrder w (f i)

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

theorem MvPowerSeries.order_prod {σ : Type u_1} {R : Type u_3} [CommSemiring R] [NoZeroDivisors R] [Nontrivial R] {ι : Type u_4} (f : ι → MvPowerSeries σ R) (s : Finset ι) : (∏ i ∈ s, f i).order = ∑ i ∈ s, (f i).order