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

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
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] :