Documentation

Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors

ZeroDivisors in a MvPowerSeries ring #

Instance #

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

TODO #

Remark #

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

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

theorem MvPowerSeries.weightedOrder_mul {σ : Type u_1} {R : Type u_2} [Semiring R] [NoZeroDivisors R] (w : σ) (f g : MvPowerSeries σ R) :
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 (∏ is, f i) = is, 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 ι) :
(∏ is, f i).order = is, (f i).order