degree_le_iff — Mathlib

English

For any polynomial f and degree bound d, f's degree bound is equivalent to each coefficient of monomials being bounded by d.

Русский

Для полинома f и границы степени d, граница степени эквивалентна для каждого монома.

LaTeX

$$$m.degree f \\preceq d \\iff \\forall c \\in f.support, c \\preceq d$$$

Lean4

theorem degree_le_iff {f : MvPolynomial σ R} {d : σ →₀ ℕ} : m.degree f ≼[m] d ↔ ∀ c ∈ f.support, c ≼[m] d :=
  by
  unfold degree
  simp only [AddEquiv.apply_symm_apply, Finset.sup_le_iff, mem_support_iff, ne_eq]

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