restrictDegree — Mathlib

English

restrictDegree(m) is the submodule of polynomials such that the degree with respect to each variable is ≤ m.

Русский

restrictDegree(m) — подмодуль полиномов, у которых степень по каждой переменной не превосходит m.

LaTeX

$$$\\mathrm{restrictDegree}(m) = \\mathrm{restrictSupport}\\ (R,\\{ n : (n(i) \\le m)\\ for\\ all\\ i\\})$$$

Lean4

/-- The submodule of polynomials such that the degree with respect to each individual variable is
less than or equal to `m`. -/
def restrictDegree (m : ℕ) : Submodule R (MvPolynomial σ R) :=
  restrictSupport R {n | ∀ i, n i ≤ m}

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