Commit 2021-09-22 12:11 a994071f

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.