Theorems · Theorem · commutative algebra

PowerSeries.IsWeierstrassDivisorAt.eq_zero_of_mul_eq

∀ {A : Type u_1} [inst : CommRing A] {g : PowerSeries A} {I : Ideal A},
  g.IsWeierstrassDivisorAt I →
    ∀ [IsHausdorff I A] {q : PowerSeries A} {r : Polynomial A},
      r.degree < ↑((PowerSeries.map (Ideal.Quotient.mk I)) g).order.toNat → g * q = ↑r → q = 0 ∧ r = 0

If g * q = r for some power series q and some polynomial r whose degree is < n, then q and r are all zero. This implies the uniqueness of Weierstrass division.

Defined in

Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Cited by

1 results in Mathlib

Foundations

Depth 106 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingIsHausdorff