supported — Mathlib

English

The set of polynomials whose variables lie in a subset s ⊆ σ is the subalgebra generated by X restricted to s; formally, supported R s = Algebra.adjoin R (X '' s).

Русский

Множество полиномов, чьи переменные лежат в подмножество s ⊆ σ, является подалгеброй, порождённой X''s; формально supported R s = Algebra.adjoin R (X '' s).

LaTeX

$$$ \text{supported } R s = \operatorname{Algebra.adjoin}_R (X'' s) $$$

Lean4

/-- The set of polynomials whose variables are contained in `s` as a `Subalgebra` over `R`. -/
noncomputable def supported (s : Set σ) : Subalgebra R (MvPolynomial σ R) :=
  Algebra.adjoin R (X '' s)

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