English
If a nonzero residue of g exists, then there is some Weierstrass factorization g = f h.
Русский
Если образ g в остаточном поле не нулевой, существует факторизация g = f h по Вейершстрасу.
LaTeX
$$$\exists f,h: g = f h \;\land\; f \text{ distinguished},\; h \text{ unit}$$$
Lean4
@[simp]
theorem weierstrassDistinguished_mul (hg : (g * g').map (IsLocalRing.residue A) ≠ 0) :
(g * g').weierstrassDistinguished hg =
g.weierstrassDistinguished (fun h ↦ hg (by simp [h])) * g'.weierstrassDistinguished (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')).1
