# Documentation

Mathlib.RingTheory.MvPolynomial.Basic

# 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

theorem MvPolynomial.mapRange_eq_map (σ : Type u) {R : Type u_1} {S : Type u_2} [] [] (p : ) (f : R →+* S) :
Finsupp.mapRange f (_ : f 0 = 0) p = ↑() p
def MvPolynomial.restrictTotalDegree (σ : Type u) (R : Type v) [] (m : ) :

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

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.

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

The monomials form a basis on MvPolynomial σ R.

Instances For
@[simp]
theorem MvPolynomial.coe_basisMonomials (σ : Type u) (R : Type v) [] :
↑() = fun s => ↑() 1
theorem MvPolynomial.linearIndependent_X (σ : Type u) (R : Type v) [] :
LinearIndependent R MvPolynomial.X
noncomputable def Polynomial.basisMonomials (R : Type v) [] :
Basis R ()

The monomials form a basis on R[X].

Instances For
@[simp]
theorem Polynomial.coe_basisMonomials (R : Type v) [] :
= fun s => ↑() 1