English
If two divisions of f by g yield pairs (q,r) and (q',r'), then q = q' and r = r'.
Русский
Если две пары деления f по g дают (q,r) и (q',r'), то q = q' и r = r'.
LaTeX
$$If f.IsWeierstrassDivision g q r and f.IsWeierstrassDivision g q' r', then q = q' and r = r'.$$
Lean4
/-- The quotient `q` and the remainder `r` in the Weierstrass division are unique.
This result is stated using two `PowerSeries.IsWeierstrassDivision` assertions, and only requires
the ring being Hausdorff with respect to the maximal ideal. If you want `q` and `r` equal to
`f /ʷ g` and `f %ʷ g`, use `PowerSeries.IsWeierstrassDivision.unique`
instead, which requires the ring being complete with respect to the maximal ideal. -/
theorem elim [IsHausdorff (IsLocalRing.maximalIdeal A) A] {q q' : A⟦X⟧} {r r' : A[X]}
(H : f.IsWeierstrassDivision g q r) (H2 : f.IsWeierstrassDivision g q' r') : q = q' ∧ r = r' :=
(IsWeierstrassDivisor.of_map_ne_zero hg).eq_of_mul_add_eq_mul_add H.1 H2.1 (H.2.symm.trans H2.2)
