Polynomials supported by a set of variables #

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

Main definitions #

Tags #

variables, polynomial, vars

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

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

Instances For
    noncomputable def MvPolynomial.supportedEquivMvPolynomial {σ : Type u_1} {R : Type u} [CommSemiring R] (s : Set σ) :

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

    Instances For
      theorem MvPolynomial.supportedEquivMvPolynomial_symm_C {σ : Type u_1} {R : Type u} [CommSemiring R] (s : Set σ) (x : R) :
      ↑(AlgEquiv.symm (MvPolynomial.supportedEquivMvPolynomial s)) (MvPolynomial.C x) = ↑(algebraMap R { x // x MvPolynomial.supported R s }) x
      theorem MvPolynomial.mem_supported {σ : Type u_1} {R : Type u} [CommSemiring R] {p : MvPolynomial σ R} {s : Set σ} :
      theorem MvPolynomial.supported_eq_vars_subset {σ : Type u_1} {R : Type u} [CommSemiring R] {s : Set σ} :
      theorem MvPolynomial.supported_eq_adjoin_X {σ : Type u_1} {R : Type u} [CommSemiring R] (s : Set σ) :
      MvPolynomial.supported R s = Algebra.adjoin R (MvPolynomial.X '' s)
      theorem MvPolynomial.supported_univ {σ : Type u_1} {R : Type u} [CommSemiring R] :
      theorem MvPolynomial.supported_mono {σ : Type u_1} {R : Type u} [CommSemiring R] {s : Set σ} {t : Set σ} (st : s t) :
      theorem MvPolynomial.X_mem_supported {σ : Type u_1} {R : Type u} [CommSemiring R] {s : Set σ} [Nontrivial R] {i : σ} :
      theorem MvPolynomial.exists_restrict_to_vars {σ : Type u_1} {s : Set σ} (R : Type u_3) [CommRing R] {F : MvPolynomial σ } (hF : ↑(MvPolynomial.vars F) s) :
      f, ∀ (x : σR), f (x Subtype.val) = ↑(MvPolynomial.aeval x) F