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 #


Generalise to noncommutative (semi)rings

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

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

Instances For

    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_restrictDegree (σ : Type u) {R : Type v} [CommSemiring R] (p : MvPolynomial σ R) (n : ) :
      p MvPolynomial.restrictDegree σ R n ∀ (s : σ →₀ ), s p∀ (i : σ), s i n

      The monomials form a basis on MvPolynomial σ R.

      Instances For
        theorem MvPolynomial.linearIndependent_X (σ : Type u) (R : Type v) [CommSemiring R] :
        LinearIndependent R MvPolynomial.X
        noncomputable def Polynomial.basisMonomials (R : Type v) [CommSemiring R] :

        The monomials form a basis on R[X].

        Instances For