Monomial basis for algebra extensions

@[simp]

theorem Polynomial.sum_degreeLT_monomial_eq_subtype {L : Type u_2} [Field L] {n : ℕ} (p : ↥(degreeLT L n)) : ⟨(↑p).sum fun (n : ℕ) (a : L) => (monomial n) a, ⋯⟩ = p

noncomputable def Polynomial.monomialBasisOfDegreeLT {L : Type u_2} [Field L] {n : ℕ} : Module.Basis (Fin n) L ↥(degreeLT L n)

theorem Polynomial.finrank_degreeLT_n {L : Type u_2} [Field L] (n : ℕ) : Module.finrank L ↥(degreeLT L n) = n

instance Polynomial.finiteDimensional_degreeLT {L : Type u_2} [Field L] {n : ℕ} (h_n_pos : 0 < n) : FiniteDimensional L ↥(degreeLT L n)