mathlib

547bf551 - feat(data/complex/module): transfer all `has_scalar ℝ` structures to `ℂ` (#6562)

feat(data/complex/module): transfer all `has_scalar ℝ` structures to `ℂ` (#6562) This provides (for an `R` with the same instance on `ℝ`) the instances: * `has_scalar R ℂ` * `is_scalar_tower R S ℂ` * `smul_comm_class R S ℂ` * `mul_action R ℂ` * `distrib_mul_action R ℂ` * `semimodule R ℂ` * `algebra R ℂ` * `normed_algebra R ℂ` This has the downside that `smul_coe` is no longer a `rfl` lemma, but means that `ℂ` is automatically an algebra over `ℝ≥0`. It renames `smul_re` and `smul_im` to `of_real_mul_re` and `of_real_mul_im`, since the previous statements did not use `smul` at all, and renaming frees up these names for lemmas which _do_ use `smul`. This removes `normed_space.restrict_scalars_real E` (implemented as `normed_space.restrict_scalars ℝ ℂ E`) as: * As an instance, it now causes unwanted diamonds * After downgrading to a def, it is never used * The docs for `normed_space.restrict_scalars` suggest judicious use, and that if you want this instance you should use the type synonym `semimodule.restrict_scalars ℝ ℂ E` which will have this instance for free.