degree_lt_iff — Mathlib

English

If 0 ≺ d in the monomial order, then m.degree f ≺ d iff every support monomial c satisfies c ≺ d.

Русский

Если 0 превосходит d по монотору, то m.degree f < d тогда и только тогда, когда каждый моном в поддержке удовлетворяет c < d.

LaTeX

$$$0 \\prec_{m} d \\Rightarrow m.degree f \\prec_{m} d \\iff \\forall c \\in f.support, c \\prec_{m} d$$$

Lean4

theorem degree_lt_iff {f : MvPolynomial σ R} {d : σ →₀ ℕ} (hd : 0 ≺[m] d) :
    m.degree f ≺[m] d ↔ ∀ c ∈ f.support, c ≺[m] d :=
  by
  simp only [map_zero] at hd
  unfold degree
  simp only [AddEquiv.apply_symm_apply]
  exact Finset.sup_lt_iff hd

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