mathlib documentation

data.mv_polynomial.supported

Polynomials supported by a set of variables #

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

Main definitions #

Tags #

variables, polynomial, vars

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

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

Equations
noncomputable def mv_polynomial.supported_equiv_mv_polynomial {σ : Type u_1} {R : Type u} [comm_semiring R] (s : set σ) :

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

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