32 Several complex variables and analytic spaces

TheoremWeierstrass preparation theorem#

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.

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

Sources

• Mathlib documentation: PowerSeries.exists_isWeierstrassFactorization
• Source of PowerSeries.exists_isWeierstrassFactorization in Mathlib/RingTheory/PowerSeries/WeierstrassPreparation.lean
• 1000+ theorems list: Q3527219
• 1000+ theorems project: Q3527219
• Wikipedia: Weierstrass preparation theorem
• Wikidata: Q3527219

MathlibPowerSeries.exists_isWeierstrassFactorization

Uses 8

Statement usesAssociative algebra over a commutative ring · Field · Linear map · Local ring · Power series · Quotient ring · Quotient space (Fundamentals) · Rational number

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.