English
If two Weierstrass factorizations of g exist, then the distinguished polynomial and the unit are unique, i.e., f,h are determined up to the stated correspondence.
Русский
Если существуют две факторизации Вейершстраса g, то отличительная часть и еденица определяются однозначно.
LaTeX
$$$(f,h) = (f',h')$ whenever $g = f h = f' h'$ with the same residue conditions.$$
Lean4
/-- The `f` and `h` in the Weierstrass preparation theorem are unique.
This result is stated using two `PowerSeries.IsWeierstrassFactorization` assertions, and only
requires the ring being Hausdorff with respect to the maximal ideal. If you want `f` and `h` equal
to `PowerSeries.weierstrassDistinguished` and `PowerSeries.weierstrassUnit`,
use `PowerSeries.IsWeierstrassFactorization.unique` instead, which requires the ring being
complete with respect to the maximal ideal. -/
theorem elim [IsHausdorff (IsLocalRing.maximalIdeal A) A] {g : A⟦X⟧} {f f' : A[X]} {h h' : A⟦X⟧}
(H : g.IsWeierstrassFactorization f h) (H2 : g.IsWeierstrassFactorization f' h') : f = f' ∧ h = h' :=
by
obtain ⟨h1, h2⟩ := H.isWeierstrassDivision.elim H.map_ne_zero H2.isWeierstrassDivision
rw [← Units.ext_iff, inv_inj, Units.ext_iff] at h1
exact ⟨by simpa using h2, h1⟩
