restrictSupport — Mathlib

English

restrictSupport is the submodule consisting of polynomials whose support lies inside a given set s.

Русский

restrictSupport — это подмодуль, состоящий из полиномов, опора которых лежит внутри заданного множества s.

LaTeX

$$$p \\in \\mathrm{restrictSupport}(R,s) \\iff p.{\\text{support}} \\subseteq s$$$

Lean4

/-- The submodule of polynomials that are sum of monomials in the set `s`. -/
def restrictSupport (s : Set (σ →₀ ℕ)) : Submodule R (MvPolynomial σ R) :=
  Finsupp.supported _ _ s

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