mathlib3

57fda28f - refactor(data/polynomial/degree/definitions): Remove hypothesis of nat_degree_X_pow_sub_C (#6628)