restrictTotalDegree — Mathlib

English

restrictTotalDegree(m) is the submodule of polynomials of total degree at most m.

Русский

restrictTotalDegree(m) — подмодуль полиномов суммарной степени не более m.

LaTeX

$$$\\mathrm{restrictTotalDegree}(m) = \\mathrm{restrictSupport}\\ (R,\{ n : (n.sum (\\lambda _ e, e)) \\le m\\})$$$

Lean4

/-- The submodule of polynomials of total degree less than or equal to `m`. -/
def restrictTotalDegree (m : ℕ) : Submodule R (MvPolynomial σ R) :=
  restrictSupport R {n | (n.sum fun _ e => e) ≤ m}

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