Theorems · Theorem · commutative algebra

PowerSeries.IsWeierstrassDivision.unique

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

If q and r are quotient and remainder in the Weierstrass division f / g, then they are equal to f /ʷ g and f %ʷ g.

Defined in

Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommRingIsLocalRingIsAdicComplete