mathlib documentation

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 #

Main statements #

TODO #

Generalise to noncommutative (semi)rings

@[protected, instance]
def mv_polynomial.char_p (σ : Type u) (R : Type v) [comm_ring R] (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 : mv_polynomial σ R) (f : R →+* S) :
def mv_polynomial.restrict_total_degree (σ : Type u) (R : Type v) [comm_ring R] (m : ) :

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 : ) :

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_degree (σ : Type u) {R : Type v} [comm_ring R] (p : mv_polynomial σ R) (n : ) :
p mv_polynomial.restrict_degree σ 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 : mv_polynomial σ R) (n : ) :
noncomputable def mv_polynomial.basis_monomials (σ : Type u) (R : Type v) [comm_ring 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] :
noncomputable def polynomial.basis_monomials (R : Type v) [comm_ring R] :

The monomials form a basis on polynomial R.

Equations