mathlib

7a3ae977 - feat(data/polynomial/laurent): add inductions for Laurent polynomials (#14005)

feat(data/polynomial/laurent): add inductions for Laurent polynomials (#14005) This PR introduces two induction principles for Laurent polynomials and uses them to show that `T` commutes with everything.