mathlib

c7a51977 - feat(data/polynomial/degree/definitions): `polynomial.degree_C_mul_X_le` (#7659)