mathlib3 documentation


Polynomials supported by a set of variables #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

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 σ} :
theorem mv_polynomial.supported_mono {σ : Type u_1} {R : Type u} [comm_semiring R] {s t : set σ} (st : s t) :
theorem mv_polynomial.X_mem_supported {σ : Type u_1} {R : Type u} [comm_semiring R] {s : set σ} [nontrivial R] {i : σ} :
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