mathlib3

e574b1a4 - feat(data/polynomial/basic): add to_finsupp_C_mul_X_pow lemmas (#17794)