Basis of a polynomial ring

noncomputable 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

• Polynomial.basisMonomials R = { repr := Polynomial.toFinsuppIsoLinear R ≪≫ₗ AddMonoidAlgebra.coeffLinearEquiv R }

@[simp]

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