English
Let f,g ∈ R[X], with g monic, and let q,r ∈ R[X] satisfy f = g q + r and deg r < deg g. Then the quotient and remainder are determined uniquely: f /ₘ g = q and f %ₘ g = r.
Русский
Пусть f, g ∈ R[X], g мономический, и пусть q, r ∈ R[X] удовлетворяют f = g q + r и deg r < deg g. Тогда частное и остаток однозначны: f /ₘ g = q и f %ₘ g = r.
LaTeX
$$$$ g \\text{ мон} =\\,\\mathrm{Monic}\\; g \\;\\land\\; (r + g q = f) \\land \\operatorname{deg} r < \\operatorname{deg} g \\Rightarrow \\; f /ₘ g = q \\land f %ₘ g = r. $$$$
Lean4
theorem div_modByMonic_unique {f g} (q r : R[X]) (hg : Monic g) (h : r + g * q = f ∧ degree r < degree g) :
f /ₘ g = q ∧ f %ₘ g = r := by
nontriviality R
have h₁ : r - f %ₘ g = -g * (q - f /ₘ g) :=
eq_of_sub_eq_zero
(by
rw [← sub_eq_zero_of_eq (h.1.trans (modByMonic_add_div f hg).symm)]
simp [mul_add, sub_eq_add_neg, add_comm, add_left_comm, add_assoc])
have h₂ : degree (r - f %ₘ g) = degree (g * (q - f /ₘ g)) := by simp [h₁]
have h₄ : degree (r - f %ₘ g) < degree g :=
calc
degree (r - f %ₘ g) ≤ max (degree r) (degree (f %ₘ g)) := degree_sub_le _ _
_ < degree g := max_lt_iff.2 ⟨h.2, degree_modByMonic_lt _ hg⟩
have h₅ : q - f /ₘ g = 0 :=
_root_.by_contradiction fun hqf =>
not_le_of_gt h₄ <|
calc
degree g ≤ degree g + degree (q - f /ₘ g) :=
by
rw [degree_eq_natDegree hg.ne_zero, degree_eq_natDegree hqf]
norm_cast
exact Nat.le_add_right _ _
_ = degree (r - f %ₘ g) := by rw [h₂, degree_mul']; simpa [Monic.def.1 hg]
exact ⟨Eq.symm <| eq_of_sub_eq_zero h₅, Eq.symm <| eq_of_sub_eq_zero <| by simpa [h₅] using h₁⟩
