English
Let f,g be polynomials in the multivariate polynomial ring MvPolynomial over a commutative ring R, with a MonomialOrder m. If the degree of g is strictly below the degree of f in the order m (i.e. m.degree g ≺[m] m.degree f), then the leading coefficient of f − g equals the leading coefficient of f.
Русский
Пусть f,g — многочлены в кольце MvPolynomial σ R над коммутативным кольцом R, и задан порядок мономов m. Если deg_m g строго меньше deg_m f по порядку m (deg g ≺ deg f), то ведущий коэффициент f − g равен ведущему коэффициенту f.
LaTeX
$$$ m.degree\; g \;\prec[{m}]\; m.degree\; f \;\Rightarrow\; m.leadingCoeff (f - g) = m.leadingCoeff f $$$
Lean4
theorem leadingCoeff_sub_of_lt {f g : MvPolynomial σ R} (h : m.degree g ≺[m] m.degree f) :
m.leadingCoeff (f - g) = m.leadingCoeff f := by
rw [sub_eq_add_neg]
apply leadingCoeff_add_of_lt
simp only [degree_neg, h]
