degree_monomial_le — Mathlib

English

The degree of a monomial is bounded by its exponent vector: degree(monomial d c) ≤ d.

Русский

Степень монома ограничена по вектору экспонентов: deg(monomial d c) ≤ d.

LaTeX

$$$m.degree(\\text{monomial } d c) \\preceq_{m} d$$$

Lean4

theorem degree_monomial_le {d : σ →₀ ℕ} (c : R) : m.degree (monomial d c) ≼[m] d :=
  by
  simp only [degree, AddEquiv.apply_symm_apply]
  apply le_trans (Finset.sup_mono support_monomial_subset)
  simp only [Finset.sup_singleton, le_refl]

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