mathlib3

0ad279c1 - feat(data/complex/module): get `smul_comm_class ℝ M E` from the one for `ℂ` (#16513)

feat(data/complex/module): get `smul_comm_class ℝ M E` from the one for `ℂ` (#16513) This makes it so all the pieces are in places to realize a non-unital `ℂ`-algebra as a non-unital `ℝ`-algebra. Co-authored-by: Eric Wieser <wieser.eric@gmail.com>