mathlib3

d5be9f38 - refactor(data/mv_polynomial): move `smul` lemmas into basic.lean (#4097)

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`.