English
Division by a monic polynomial does not change the leading coefficient provided deg q ≤ deg p.
Русский
Деление на моноик не меняет ведущий коэффициент при условии deg q ≤ deg p.
LaTeX
$$$ (p /ₘ q).leadingCoeff = p.leadingCoeff \quad\text{if } q.Monic \text{ and } deg q \le deg p $$$
Lean4
/-- Division by a monic polynomial doesn't change the leading coefficient. -/
theorem leadingCoeff_divByMonic_of_monic (hmonic : q.Monic) (hdegree : q.degree ≤ p.degree) :
(p /ₘ q).leadingCoeff = p.leadingCoeff := by
nontriviality
have h : q.leadingCoeff * (p /ₘ q).leadingCoeff ≠ 0 := by
simpa [divByMonic_eq_zero_iff hmonic, hmonic.leadingCoeff, Nat.WithBot.one_le_iff_zero_lt] using hdegree
nth_rw 2 [← modByMonic_add_div p hmonic]
rw [leadingCoeff_add_of_degree_lt, leadingCoeff_monic_mul hmonic]
rw [degree_mul' h, degree_add_divByMonic hmonic hdegree]
exact (degree_modByMonic_lt p hmonic).trans_le hdegree
