Commit 2025-02-24 16:10 4020c36b

feat(Polynomial): polynomial sequences are bases for R[X] (#20846) We define polynomial sequences -- that is, sequences of polynomials where the ith polynomial has degree i. We do not yet refactor any existing polynomial sequences to go via this proof (e.g. for the usual monomial basis which has its own proof already in Mathlib).