# mathlibdocumentation

ring_theory.mv_polynomial.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 #

• restrict_total_degree σ R m: the subspace of multivariate polynomials indexed by σ over the commutative ring R of total degree at most m.
• restrict_degree σ 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 ring of positive characteristic has positive characteristic.
• basis_monomials: shows that the monomials form a basis of the vector space of multivariate polynomials.

## TODO #

Generalise to noncommutative (semi)rings

@[protected, instance]
def mv_polynomial.char_p (σ : Type u) (R : Type v) [comm_ring R] (p : ) [ p] :
char_p R) p
theorem mv_polynomial.map_range_eq_map (σ : Type u) {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] (p : R) (f : R →+* S) :
p = p
def mv_polynomial.restrict_total_degree (σ : Type u) (R : Type v) [comm_ring R] (m : ) :
R)

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

Equations
def mv_polynomial.restrict_degree (σ : Type u) (R : Type v) [comm_ring R] (m : ) :
R)

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

Equations
theorem mv_polynomial.mem_restrict_total_degree (σ : Type u) {R : Type v} [comm_ring R] (m : ) (p : R) :
theorem mv_polynomial.mem_restrict_degree (σ : Type u) {R : Type v} [comm_ring R] (p : R) (n : ) :
∀ (s : σ →₀ ), s p.support∀ (i : σ), s i n
theorem mv_polynomial.mem_restrict_degree_iff_sup (σ : Type u) {R : Type v} [comm_ring R] (p : R) (n : ) :
∀ (i : σ), n
noncomputable def mv_polynomial.basis_monomials (σ : Type u) (R : Type v) [comm_ring R] :
basis →₀ ) R R)

The monomials form a basis on mv_polynomial σ R.

Equations
@[simp]
theorem mv_polynomial.coe_basis_monomials (σ : Type u) (R : Type v) [comm_ring R] :
= λ (s : σ →₀ ),
theorem mv_polynomial.linear_independent_X (σ : Type u) (R : Type v) [comm_ring R] :
noncomputable def polynomial.basis_monomials (R : Type v) [comm_ring R] :
R (polynomial R)

The monomials form a basis on polynomial R.

Equations
@[simp]
theorem polynomial.coe_basis_monomials (R : Type v) [comm_ring R] :
= λ (s : ), 1