mathlib

a994071f - chore(data/complex/module): rename `complex.smul_coe` to `real_smul` (#9326)

chore(data/complex/module): rename `complex.smul_coe` to `real_smul` (#9326) * the name was misleading b/c there is no `coe` in the LHS; * add `complex.coe_smul`: given `x : ℝ` and `y : E`, we have `(x : ℂ) • y = x • y`; * add `normed_space.complex_to_real`.