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)