Commit 2020-09-10 13:02 d5be9f38

refactor(data/mv_polynomial): move smul lemmas into basic.lean (#4097) C_mul', smul_eq_C_mul and smul_eval seemed a bit out of place in comm_ring.lean, since they only need comm_semiring α. So I moved them to basic.lean where they probably fit in a bit better? I've also golfed the proof of smul_eq_C_mul.