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

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

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

Equations
Instances For
    source
    theorem MvPolynomial.supported_eq_range_rename {σ : Type u_1} {R : Type u} [CommSemiring R] (s : Set σ) :
    MvPolynomial.supported R s = AlgHom.range (MvPolynomial.rename Subtype.val)
    source
    noncomputable def MvPolynomial.supportedEquivMvPolynomial {σ : Type u_1} {R : Type u} [CommSemiring R] (s : Set σ) :
    ↥(MvPolynomial.supported R s) ≃ₐ[R] MvPolynomial (↑s) R

    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
      source
      @[simp]
      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 ↥(MvPolynomial.supported R s)) x
      source
      @[simp]
      theorem MvPolynomial.supportedEquivMvPolynomial_symm_X {σ : Type u_1} {R : Type u} [CommSemiring R] (s : Set σ) (i : ↑s) :
      ↑((AlgEquiv.symm (MvPolynomial.supportedEquivMvPolynomial s)) (MvPolynomial.X i)) = MvPolynomial.X ↑i
      source
      theorem MvPolynomial.mem_supported {σ : Type u_1} {R : Type u} [CommSemiring R] {p : MvPolynomial σ R} {s : Set σ} :
      p ∈ MvPolynomial.supported R s ↔ ↑(MvPolynomial.vars p) ⊆ s
      source
      theorem MvPolynomial.supported_eq_vars_subset {σ : Type u_1} {R : Type u} [CommSemiring R] {s : Set σ} :
      ↑(MvPolynomial.supported R s) = {p : MvPolynomial σ R | ↑(MvPolynomial.vars p) ⊆ s}
      source
      @[simp]
      theorem MvPolynomial.mem_supported_vars {σ : Type u_1} {R : Type u} [CommSemiring R] (p : MvPolynomial σ R) :
      p ∈ MvPolynomial.supported R ↑(MvPolynomial.vars p)
      source
      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)
      source
      @[simp]
      theorem MvPolynomial.supported_univ {σ : Type u_1} {R : Type u} [CommSemiring R] :
      MvPolynomial.supported R Set.univ = ⊤
      source
      @[simp]
      theorem MvPolynomial.supported_empty {σ : Type u_1} {R : Type u} [CommSemiring R] :
      MvPolynomial.supported R ∅ = ⊥
      source
      theorem MvPolynomial.supported_mono {σ : Type u_1} {R : Type u} [CommSemiring R] {s : Set σ} {t : Set σ} (st : s ⊆ t) :
      MvPolynomial.supported R s ≤ MvPolynomial.supported R t
      source
      @[simp]
      theorem MvPolynomial.X_mem_supported {σ : Type u_1} {R : Type u} [CommSemiring R] {s : Set σ} [Nontrivial R] {i : σ} :
      MvPolynomial.X i ∈ MvPolynomial.supported R s ↔ i ∈ s
      source
      @[simp]
      theorem MvPolynomial.supported_le_supported_iff {σ : Type u_1} {R : Type u} [CommSemiring R] {s : Set σ} {t : Set σ} [Nontrivial R] :
      MvPolynomial.supported R s ≤ MvPolynomial.supported R t ↔ s ⊆ t
      source
      theorem MvPolynomial.supported_strictMono {σ : Type u_1} {R : Type u} [CommSemiring R] [Nontrivial R] :
      StrictMono (MvPolynomial.supported R)
      source
      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 : (↑s → R) → R), ∀ (x : σ → R), f (x ∘ Subtype.val) = (MvPolynomial.aeval x) F