# mathlibdocumentation

data.mv_polynomial.supported

# Polynomials supported by a set of variables #

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

## Main definitions #

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

## Tags #

variables, polynomial, vars

noncomputable def mv_polynomial.supported {σ : Type u_1} (R : Type u) (s : set σ) :
R)

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

Equations
theorem mv_polynomial.supported_eq_range_rename {σ : Type u_1} {R : Type u} (s : set σ) :
noncomputable def mv_polynomial.supported_equiv_mv_polynomial {σ : Type u_1} {R : Type u} (s : set σ) :

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

Equations
@[simp]
theorem mv_polynomial.supported_equiv_mv_polynomial_symm_C {σ : Type u_1} {R : Type u} (s : set σ) (x : R) :
@[simp]
theorem mv_polynomial.supported_equiv_mv_polynomial_symm_X {σ : Type u_1} {R : Type u} (s : set σ) (i : s) :
theorem mv_polynomial.mem_supported {σ : Type u_1} {R : Type u} {p : R} {s : set σ} :
(p.vars) s
theorem mv_polynomial.supported_eq_vars_subset {σ : Type u_1} {R : Type u} {s : set σ} :
= {p : | (p.vars) s}
@[simp]
theorem mv_polynomial.mem_supported_vars {σ : Type u_1} {R : Type u} (p : R) :
p
theorem mv_polynomial.supported_eq_adjoin_X {σ : Type u_1} {R : Type u} (s : set σ) :
@[simp]
theorem mv_polynomial.supported_univ {σ : Type u_1} {R : Type u}  :
@[simp]
theorem mv_polynomial.supported_empty {σ : Type u_1} {R : Type u}  :
theorem mv_polynomial.supported_mono {σ : Type u_1} {R : Type u} {s t : set σ} (st : s t) :
@[simp]
theorem mv_polynomial.X_mem_supported {σ : Type u_1} {R : Type u} {s : set σ} [nontrivial R] {i : σ} :
i s
@[simp]
theorem mv_polynomial.supported_le_supported_iff {σ : Type u_1} {R : Type u} {s t : set σ} [nontrivial R] :
s t
theorem mv_polynomial.supported_strict_mono {σ : Type u_1} {R : Type u} [nontrivial R] :
theorem mv_polynomial.exists_restrict_to_vars {σ : Type u_1} {s : set σ} (R : Type u_2) [comm_ring R] {F : } (hF : (F.vars) s) :
∃ (f : (s → R) → R), ∀ (x : σ → R), f (x coe) = F