mem_restrictTotalDegree — Mathlib

English

p belongs to restrictTotalDegree iff its total degree is ≤ m.

Русский

p принадлежит restrictTotalDegree σ R m тогда и только тогда, когда общая степень p ≤ m.

LaTeX

$$$p \\in \\mathrm{restrictTotalDegree}(\\sigma,R,m) \\\\iff p.\\mathrm{totalDegree} \\le m$$$

Lean4

theorem mem_restrictTotalDegree (p : MvPolynomial σ R) : p ∈ restrictTotalDegree σ R m ↔ p.totalDegree ≤ m :=
  by
  rw [totalDegree, Finset.sup_le_iff]
  rfl

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