# Polynomials supported by a set of variables #

This file contains the definition and lemmas about MvPolynomial.supported.

## Main definitions #

• MvPolynomial.supported : Given a set s : Set σ, supported R s is the subalgebra of MvPolynomial σ R consisting of polynomials whose set of variables is contained in s. This subalgebra is isomorphic to MvPolynomial s R.

## Tags #

variables, polynomial, vars

noncomputable def MvPolynomial.supported {σ : Type u_1} (R : Type u) [] (s : Set σ) :

The set of polynomials whose variables are contained in s as a Subalgebra over R.

Equations
Instances For
theorem MvPolynomial.supported_eq_range_rename {σ : Type u_1} {R : Type u} [] (s : Set σ) :
= (MvPolynomial.rename Subtype.val).range
noncomputable def MvPolynomial.supportedEquivMvPolynomial {σ : Type u_1} {R : Type u} [] (s : Set σ) :
≃ₐ[R] MvPolynomial (↑s) R

The isomorphism between the subalgebra of polynomials supported by s and MvPolynomial s R.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem MvPolynomial.supportedEquivMvPolynomial_symm_C {σ : Type u_1} {R : Type u} [] (s : Set σ) (x : R) :
(MvPolynomial.C x) = (algebraMap R ) x
@[simp]
theorem MvPolynomial.supportedEquivMvPolynomial_symm_X {σ : Type u_1} {R : Type u} [] (s : Set σ) (i : s) :
( ) =
theorem MvPolynomial.mem_supported {σ : Type u_1} {R : Type u} [] {p : } {s : Set σ} :
p.vars s
theorem MvPolynomial.supported_eq_vars_subset {σ : Type u_1} {R : Type u} [] {s : Set σ} :
= {p : | p.vars s}
@[simp]
theorem MvPolynomial.mem_supported_vars {σ : Type u_1} {R : Type u} [] (p : ) :
theorem MvPolynomial.supported_eq_adjoin_X {σ : Type u_1} {R : Type u} [] (s : Set σ) :
= Algebra.adjoin R (MvPolynomial.X '' s)
@[simp]
theorem MvPolynomial.supported_univ {σ : Type u_1} {R : Type u} [] :
@[simp]
theorem MvPolynomial.supported_empty {σ : Type u_1} {R : Type u} [] :
theorem MvPolynomial.supported_mono {σ : Type u_1} {R : Type u} [] {s : Set σ} {t : Set σ} (st : s t) :
@[simp]
theorem MvPolynomial.X_mem_supported {σ : Type u_1} {R : Type u} [] {s : Set σ} [] {i : σ} :
i s
@[simp]
theorem MvPolynomial.supported_le_supported_iff {σ : Type u_1} {R : Type u} [] {s : Set σ} {t : Set σ} [] :
s t
theorem MvPolynomial.supported_strictMono {σ : Type u_1} {R : Type u} [] [] :
theorem MvPolynomial.exists_restrict_to_vars {σ : Type u_1} {s : Set σ} (R : Type u_3) [] {F : } (hF : F.vars s) :
∃ (f : (sR)R), ∀ (x : σR), f (x Subtype.val) = F