degree_sub_LTerm_le — Mathlib

English

For any polynomial f and a monomial order m, the degree of the left term m.subLTerm(f) is bounded above by the degree of f with respect to m.

Русский

Для любого полинома f и порядка м, грань deg_m (m.subLTerm(f)) не превосходит deg_m f.

LaTeX

$$$m.\\deg(\\,m.\\mathrm{subLTerm}(f)\\,) \\preceq_m m.\\deg(f)$$$

Lean4

theorem degree_sub_LTerm_le (f : MvPolynomial σ R) : m.degree (m.subLTerm f) ≼[m] m.degree f :=
  by
  apply le_trans degree_sub_le
  simp only [sup_le_iff, le_refl, true_and]
  apply degree_monomial_le

Похожие утверждения