English
Let f and g be polynomials over a Ring R with g monic. Then the natural degree of the quotient f divided by g in the monic-division sense equals the difference of the natural degrees: natDegree(f /ₘ g) = natDegree(f) − natDegree(g).
Русский
Пусть f и g — многочлены над кольцом R, причём g мономический. Тогда естественная степень частного f деления на g по моному делителю равна разности степеней: natDegree(f /ₘ g) = natDegree(f) − natDegree(g).
LaTeX
$$$$ \\operatorname{natDegree}\\left(\\frac{f}{\\!\\!\\mathrm{monic}\\, g}\\right) = \\operatorname{natDegree}(f) - \\operatorname{natDegree}(g). $$$$
Lean4
theorem natDegree_divByMonic (f : R[X]) {g : R[X]} (hg : g.Monic) : natDegree (f /ₘ g) = natDegree f - natDegree g :=
by
nontriviality R
by_cases hfg : f /ₘ g = 0
· rw [hfg, natDegree_zero]
rw [divByMonic_eq_zero_iff hg] at hfg
rw [tsub_eq_zero_iff_le.mpr (natDegree_le_natDegree <| le_of_lt hfg)]
have hgf := hfg
rw [divByMonic_eq_zero_iff hg] at hgf
push_neg at hgf
have := degree_add_divByMonic hg hgf
have hf : f ≠ 0 := by
intro hf
apply hfg
rw [hf, zero_divByMonic]
rw [degree_eq_natDegree hf, degree_eq_natDegree hg.ne_zero, degree_eq_natDegree hfg, ← Nat.cast_add,
Nat.cast_inj] at this
rw [← this, add_tsub_cancel_left]
