mathlib documentation


Multivariate polynomials over commutative rings #

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

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

Main definitions #

Main statements #


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

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

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.

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 (i : σ), s i n
noncomputable def mv_polynomial.basis_monomials (σ : Type u) (R : Type v) [comm_ring R] :

The monomials form a basis on mv_polynomial σ R.

noncomputable def polynomial.basis_monomials (R : Type v) [comm_ring R] :

The monomials form a basis on R[X].