Theorems · Theorem · commutative algebra

PowerSeries.IsWeierstrassDivision.elim

∀ {A : Type u_1} [inst : CommRing A] [inst_1 : IsLocalRing A] {f g : PowerSeries A},
  (PowerSeries.map (IsLocalRing.residue A)) g ≠ 0 →
    ∀ [IsHausdorff (IsLocalRing.maximalIdeal A) A] {q q' : PowerSeries A} {r r' : Polynomial A},
      f.IsWeierstrassDivision g q r → f.IsWeierstrassDivision g q' r' → q = q' ∧ r = r'

The quotient q and the remainder r in the Weierstrass division are unique. This result is stated using two PowerSeries.IsWeierstrassDivision assertions, and only requires the ring being Hausdorff with respect to the maximal ideal. If you want q and r equal to f /ʷ g and f %ʷ g, use PowerSeries.IsWeierstrassDivision.unique instead, which requires the ring being complete with respect to the maximal ideal.

Defined in

Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Cited by

3 results in Mathlib

Foundations

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

Assumes

CommRingIsLocalRingIsHausdorff