mathlib3

45a8f6cd - feat(data/polynomial/basic): add simp lemmas X_mul_C and X_pow_mul_C (#13163)

feat(data/polynomial/basic): add simp lemmas X_mul_C and X_pow_mul_C (#13163) These lemmas are direct applications of `X_mul` and `X_pow_mul`. However, their more general version cannot be `simp` lemmas since they form loops. These versions do not, since they involve an explicit `C`. I golfed slightly a proof in `linear_algebra.eigenspace` since it was timing out. [Zulip discussion](https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/polynomial.20op_C/near/277703846)