mathlib3

f221bfd8 - feat(data/polynomial/degree/definitions): leading_coeff_X_pow_sub_C (#6633)

feat(data/polynomial/degree/definitions): leading_coeff_X_pow_sub_C (#6633) Lemma for the leading coefficient of `X ^ n - C r`. Co-authored-by: tb65536 <tb65536@users.noreply.github.com>