English
If the degree of f is nonzero, then the LT (leading term) comparison between m.subLTerm(f) and f is strict: deg_m(m.subLTerm f) < deg_m f.
Русский
Если deg_m f ≠ 0, то сравнение ведущих членов m.subLTerm(f) и f даёт строгую неравенство: deg_m(m.subLTerm f) < deg_m f.
LaTeX
$$$\\deg_m(m.\\mathrm{subLTerm}(f)) \\; <_m \\; \\deg_m(f) \\quad \\text{if } m.\\deg(f) \\neq 0$$$
Lean4
theorem degree_sub_LTerm_lt {f : MvPolynomial σ R} (hf : m.degree f ≠ 0) : m.degree (m.subLTerm f) ≺[m] m.degree f :=
by
rw [lt_iff_le_and_ne]
refine ⟨degree_sub_LTerm_le f, ?_⟩
classical
intro hf'
simp only [EmbeddingLike.apply_eq_iff_eq] at hf'
have : m.subLTerm f ≠ 0 := by
intro h
simp only [h, degree_zero] at hf'
exact hf hf'.symm
rw [← coeff_degree_ne_zero_iff (m := m), hf'] at this
apply this
simp [subLTerm, coeff_monomial, leadingCoeff]
