English
If the residue of g is nonzero, then there exist a distinguished polynomial f and a unit h such that g = f h.
Русский
Если образ g в остаточном поле не нулевой, то существуют отличительная многочлен и единица так, что g = f h.
LaTeX
$$$\exists f,h: g = f \cdot h \quad \text{with } f \text{ distinguished}, \ h \text{ a unit}$$$
Lean4
/-- **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`. -/
theorem exists_isWeierstrassFactorization (hg : g.map (IsLocalRing.residue A) ≠ 0) :
∃ f h, g.IsWeierstrassFactorization f h :=
by
obtain ⟨q, r, H⟩ := (X ^ (g.map (IsLocalRing.residue A)).order.toNat).exists_isWeierstrassDivision hg
exact ⟨_, _, H.isWeierstrassFactorization hg⟩
