English
If g has a Weierstrass factorization with distinguished f and unit h, then g equals f h.
Русский
Если g имеет факторизацию Вейершстраса с отличительной f и единицей h, то g = f h.
LaTeX
$$$g = f \cdot h$ with $f$ distinguished and $h$ a unit$$
Lean4
theorem isWeierstrassFactorization_weierstrassDistinguished_weierstrassUnit (hg : g.map (IsLocalRing.residue A) ≠ 0) :
g.IsWeierstrassFactorization (g.weierstrassDistinguished hg) (g.weierstrassUnit hg) :=
(g.exists_isWeierstrassFactorization hg).choose_spec.choose_spec
