Theorems · Theorem · commutative algebra

PowerSeries.exists_isWeierstrassFactorization

• 1000+ list: Weierstrass preparation theorem

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

Weierstrass preparation theorem ([washington_cyclotomic], Theorem 7.3): let g be a power series over a complete local ring, such that its image in the residue field is not zero. Then there exists a distinguished polynomial f and a power series h which is a unit, such that g = f * h.

Defined in

Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Cited by

4 results in Mathlib

Foundations

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

Assumes

CommRingIsLocalRingIsAdicComplete