Basis of a polynomial ring

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.

@[simp]

theorem Polynomial.coe_basisMonomials (R : Type u) [Semiring R] : ⇑(basisMonomials R) = fun (s : ℕ) => (monomial s) 1