English
There exist a distinguished polynomial f and a unit h such that g = f h for a power series g over a complete local ring with nonzero residue.
Русский
Для степенного ряда g над полем полного локального кольца существует факторизация g = f h, где f — отличительная, h — единица.
LaTeX
$$$\exists f,h: g = f h,\; f \text{ distinguished},\; h \text{ unit}$$$
Lean4
@[simp]
theorem weierstrassUnit_mul (hg : (g * g').map (IsLocalRing.residue A) ≠ 0) :
(g * g').weierstrassUnit hg =
g.weierstrassUnit (fun h ↦ hg (by simp [h])) * g'.weierstrassUnit (fun h ↦ hg (by simp [h])) :=
by
have H := g.isWeierstrassFactorization_weierstrassDistinguished_weierstrassUnit (fun h ↦ hg (by simp [h]))
have H' := g'.isWeierstrassFactorization_weierstrassDistinguished_weierstrassUnit (fun h ↦ hg (by simp [h]))
have H'' := (g * g').isWeierstrassFactorization_weierstrassDistinguished_weierstrassUnit hg
exact (H''.elim (H.mul H')).2
