mathlib

41626f7d - feat(data/polynomial/degree/definitions): add `degree_X_sub_C_le` (#16404)