English
If g q + r = g q' + r' with deg r, deg r' < n, then q = q' and r = r'.
Русский
Если g q + r = g q' + r' при deg r, deg r' < n, то q = q' и r = r'.
LaTeX
$$$ g q + r = g q' + r' \\land \\deg(r) < n \\land \\deg(r') < n \\Rightarrow q = q' \\land r = r'. $$$
Lean4
/-- If `g * q + r = g * q' + r'` for some power series `q`, `q'` and some polynomials `r`, `r'`
whose degrees are `< n`, then `q = q'` and `r = r'` are all zero.
This implies the uniqueness of Weierstrass division. -/
theorem eq_of_mul_add_eq_mul_add [IsHausdorff I A] {q q' : A⟦X⟧} {r r' : A[X]}
(hr : r.degree < (g.map (Ideal.Quotient.mk I)).order.toNat)
(hr' : r'.degree < (g.map (Ideal.Quotient.mk I)).order.toNat) (heq : g * q + r = g * q' + r') : q = q' ∧ r = r' :=
by
replace heq : g * (q - q') = ↑(r' - r) := by
rw [← eq_sub_iff_add_eq] at heq
rw [Polynomial.coe_sub, mul_sub, heq]
ring
have h := H.eq_zero_of_mul_eq (lt_of_le_of_lt (r'.degree_sub_le r) (max_lt hr' hr)) heq
simp_rw [sub_eq_zero] at h
exact ⟨h.1, h.2.symm⟩
