Documentation

Mathlib.Data.MvPolynomial.Supported

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.

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

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      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)
      @[simp]
      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) :
      @[simp]
      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 : (sR)R), ∀ (x : σR), f (x Subtype.val) = (MvPolynomial.aeval x) F