# Documentation

Mathlib.Data.MvPolynomial.Supported

# 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.

Instances For
theorem MvPolynomial.supported_eq_range_rename {σ : Type u_1} {R : Type u} [] (s : Set σ) :
noncomputable def MvPolynomial.supportedEquivMvPolynomial {σ : Type u_1} {R : Type u} [] (s : Set σ) :
{ x // } ≃ₐ[R] MvPolynomial (s) R

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

Instances For
@[simp]
theorem MvPolynomial.supportedEquivMvPolynomial_symm_C {σ : Type u_1} {R : Type u} [] (s : Set σ) (x : R) :
↑() (MvPolynomial.C x) = ↑(algebraMap R { x // }) 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 σ} :
↑() s
theorem MvPolynomial.supported_eq_vars_subset {σ : Type u_1} {R : Type u} [] {s : Set σ} :
↑() = {p | ↑() 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 : ↑() s) :
f, ∀ (x : σR), f (x Subtype.val) = ↑() F