# Multivariate polynomials over commutative rings #

This file contains basic facts about multivariate polynomials over commutative rings, for example that the monomials form a basis.

## Main definitions #

• restrictTotalDegree σ R m: the subspace of multivariate polynomials indexed by σ over the commutative ring R of total degree at most m.
• restrictDegree σ R m: the subspace of multivariate polynomials indexed by σ over the commutative ring R such that the degree in each individual variable is at most m.

## Main statements #

• The multivariate polynomial ring over a commutative semiring of characteristic p has characteristic p, and similarly for CharZero.
• basisMonomials: shows that the monomials form a basis of the vector space of multivariate polynomials.

## TODO #

Generalise to noncommutative (semi)rings

instance MvPolynomial.instCharP (σ : Type u) (R : Type v) [] (p : ) [CharP R p] :
CharP () p
Equations
• =
instance MvPolynomial.instCharZero (σ : Type u) (R : Type v) [] [] :
Equations
• =
theorem MvPolynomial.mapRange_eq_map (σ : Type u) {R : Type u_1} {S : Type u_2} [] [] (p : ) (f : R →+* S) :
Finsupp.mapRange f p = () p
def MvPolynomial.restrictSupport {σ : Type u} (R : Type v) [] (s : Set (σ →₀ )) :

The submodule of polynomials that are sum of monomials in the set s.

Equations
Instances For
def MvPolynomial.basisRestrictSupport {σ : Type u} (R : Type v) [] (s : Set (σ →₀ )) :
Basis (s) R

restrictSupport R s has a canonical R-basis indexed by s.

Equations
• = { repr := }
Instances For
theorem MvPolynomial.restrictSupport_mono {σ : Type u} (R : Type v) [] {s : Set (σ →₀ )} {t : Set (σ →₀ )} (h : s t) :
def MvPolynomial.restrictTotalDegree (σ : Type u) (R : Type v) [] (m : ) :

The submodule of polynomials of total degree less than or equal to m.

Equations
Instances For
def MvPolynomial.restrictDegree (σ : Type u) (R : Type v) [] (m : ) :

The submodule of polynomials such that the degree with respect to each individual variable is less than or equal to m.

Equations
Instances For
theorem MvPolynomial.mem_restrictTotalDegree (σ : Type u) {R : Type v} [] (m : ) (p : ) :
p.totalDegree m
theorem MvPolynomial.mem_restrictDegree (σ : Type u) {R : Type v} [] (p : ) (n : ) :
p sp.support, ∀ (i : σ), s i n
theorem MvPolynomial.mem_restrictDegree_iff_sup (σ : Type u) {R : Type v} [] [] (p : ) (n : ) :
p ∀ (i : σ), Multiset.count i p.degrees n
def MvPolynomial.basisMonomials (σ : Type u) (R : Type v) [] :
Basis (σ →₀ ) R ()

The monomials form a basis on MvPolynomial σ R.

Equations
• = Finsupp.basisSingleOne
Instances For
@[simp]
theorem MvPolynomial.coe_basisMonomials (σ : Type u) (R : Type v) [] :
= fun (s : σ →₀ ) =>
instance MvPolynomial.instFree (σ : Type u) (R : Type v) [] :

The R-module MvPolynomial σ R is free.

Equations
• =
theorem MvPolynomial.linearIndependent_X (σ : Type u) (R : Type v) [] :
LinearIndependent R MvPolynomial.X
Equations
• =
Equations
• =
noncomputable def Polynomial.basisMonomials (R : Type v) [] :
Basis R ()

The monomials form a basis on R[X].

Equations
• = { repr := .toLinearEquiv }
Instances For
@[simp]
theorem Polynomial.coe_basisMonomials (R : Type v) [] :
= fun (s : ) => 1