Commit 2025-06-18 15:55 7aa3679e

View on Github →

feat(RingTheory): basis for Polynomial.degreeLT (#26091) Linear algebra results about the module R[x]_n of polynomials with degree < n.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Polynomial/Taylor.lean

modified theorem Polynomial.coe_taylorEquiv

added theorem Polynomial.toAlgHom_taylorEquiv

Created Mathlib/RingTheory/Polynomial/DegreeLT.lean

added theorem Polynomial.comap_taylorEquiv_degreeLT

added theorem Polynomial.degreeLT.addLinearEquiv_apply'

added theorem Polynomial.degreeLT.addLinearEquiv_apply

added theorem Polynomial.degreeLT.addLinearEquiv_apply_fst

added theorem Polynomial.degreeLT.addLinearEquiv_apply_snd

added theorem Polynomial.degreeLT.addLinearEquiv_castAdd

added theorem Polynomial.degreeLT.addLinearEquiv_natAdd

added theorem Polynomial.degreeLT.addLinearEquiv_symm_apply'

added theorem Polynomial.degreeLT.addLinearEquiv_symm_apply

added theorem Polynomial.degreeLT.addLinearEquiv_symm_apply_inl

added theorem Polynomial.degreeLT.addLinearEquiv_symm_apply_inl_basis

added theorem Polynomial.degreeLT.addLinearEquiv_symm_apply_inr

added theorem Polynomial.degreeLT.addLinearEquiv_symm_apply_inr_basis

added theorem Polynomial.degreeLT.basisProd_castAdd

added theorem Polynomial.degreeLT.basisProd_natAdd

added theorem Polynomial.degreeLT.basis_repr

added theorem Polynomial.degreeLT.basis_val

added theorem Polynomial.det_taylorLinearEquiv

added theorem Polynomial.det_taylorLinearEquiv_toLinearMap

added theorem Polynomial.map_taylorEquiv_degreeLT

added theorem Polynomial.taylorLinearEquiv_symm

added theorem Polynomial.taylor_mem_degreeLT