mathlib3

d5de8eac - feat(data/polynomial): add some simp attributes and commuted versions of coeff_mul_X_pow (#10868)

feat(data/polynomial): add some simp attributes and commuted versions of coeff_mul_X_pow (#10868) I couldn't find these before and accidentally rewrote them from scratch, I think part of the reason is that I would have expected all of these vesions to be simp lemmas, so we add some more versions of these lemmas and tag everything as simp. From flt-regular