Documentation

Mathlib.Algebra.Polynomial.Basis

Basis of a polynomial ring #

source
def Polynomial.basisMonomials (R : Type u) [Semiring R] :
Module.Basis ℕ R (Polynomial R)

The monomials form a basis on R[X]. To get the rank of a polynomial ring, use this and Basis.mk_eq_rank.

Equations
    Instances For
      source
      @[simp]
      theorem Polynomial.coe_basisMonomials (R : Type u) [Semiring R] :
      ⇑(basisMonomials R) = fun (s : ℕ) => (monomial s) 1