Commit 2021-03-10 20:43 547bf551

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.