Theorems · Theorem · commutative algebra

PowerSeries.exists_isWeierstrassDivision

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

Weierstrass division ([washington_cyclotomic], Proposition 7.2): let f, g be power series over a complete local ring, such that the image of g in the residue field is not zero. Let n be the order of the image of g in the residue field. Then there exists a power series q and a polynomial r of degree < n, such that f = g * q + r.

Defined in

Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingIsLocalRingIsAdicComplete