Theorem Polynomial.degreeLT.addLinearEquiv_symm_apply_inr_basis

Modification history

2025-06-18 15:55
Mathlib/RingTheory/Polynomial/DegreeLT.lean
feat(RingTheory): basis for Polynomial.degreeLT (#26091) …
Added Polynomial.degreeLT.addLinearEquiv_symm_apply_inr_basisView on Github →