Commit 2021-12-20 09:01 d5de8eac

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