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.

src/analysis/complex/basic.lean

@@ -48,9 +48,9 @@ instance : normed_field ℂ :=
 instance : nondiscrete_normed_field ℂ :=
 { non_trivial := ⟨2, by simp [norm]; norm_num⟩ }
 
-instance normed_algebra_over_reals : normed_algebra ℝ ℂ :=
-{ norm_algebra_map_eq := abs_of_real,
-  ..complex.algebra_over_reals }
+instance {R : Type*} [normed_field R] [normed_algebra R ℝ] : normed_algebra R ℂ :=
+{ norm_algebra_map_eq := λ x, (abs_of_real $ algebra_map R ℝ x).trans (norm_algebra_map_eq ℝ x),
+  to_algebra := complex.algebra }
 
 @[simp] lemma norm_eq_abs (z : ℂ) : ∥z∥ = abs z := rfl
 
@@ -71,11 +71,6 @@ by rw [norm_real, real.norm_eq_abs]
 lemma norm_int_of_nonneg {n : ℤ} (hn : 0 ≤ n) : ∥(n : ℂ)∥ = n :=
 by rw [norm_int, _root_.abs_of_nonneg]; exact int.cast_nonneg.2 hn
 
-/-- A complex normed vector space is also a real normed vector space. -/
-@[priority 900]
-instance normed_space.restrict_scalars_real (E : Type*) [normed_group E] [normed_space ℂ E] :
-  normed_space ℝ E := normed_space.restrict_scalars ℝ ℂ E
-
 open continuous_linear_map
 
 /-- Continuous linear map version of the real part function, from `ℂ` to `ℝ`. -/

src/analysis/special_functions/pow.lean

@@ -101,7 +101,7 @@ begin
   suffices : im (log x * n⁻¹) ∈ set.Ioc (-π) π,
   { rw [← cpow_nat_cast, ← cpow_mul _ this.1 this.2, inv_mul_cancel, cpow_one],
     exact_mod_cast hn.ne' },
-  rw [mul_comm, ← of_real_nat_cast, ← of_real_inv, smul_im, ← div_eq_inv_mul],
+  rw [mul_comm, ← of_real_nat_cast, ← of_real_inv, of_real_mul_im, ← div_eq_inv_mul],
   have hn' : 0 < (n : ℝ), by assumption_mod_cast,
   have hn1 : 1 ≤ (n : ℝ), by exact_mod_cast (nat.succ_le_iff.2 hn),
   split,

src/data/complex/basic.lean

@@ -106,10 +106,10 @@ instance : has_mul ℂ := ⟨λ z w, ⟨z.re * w.re - z.im * w.im, z.re * w.im +
 @[simp] lemma mul_im (z w : ℂ) : (z * w).im = z.re * w.im + z.im * w.re := rfl
 @[simp, norm_cast] lemma of_real_mul (r s : ℝ) : ((r * s : ℝ) : ℂ) = r * s := ext_iff.2 $ by simp
 
-lemma smul_re (r : ℝ) (z : ℂ) : (↑r * z).re = r * z.re := by simp
-lemma smul_im (r : ℝ) (z : ℂ) : (↑r * z).im = r * z.im := by simp
-lemma of_real_smul (r : ℝ) (z : ℂ) : (↑r * z) = ⟨r * z.re, r * z.im⟩ :=
-ext (smul_re _ _) (smul_im _ _)
+lemma of_real_mul_re (r : ℝ) (z : ℂ) : (↑r * z).re = r * z.re := by simp
+lemma of_real_mul_im (r : ℝ) (z : ℂ) : (↑r * z).im = r * z.im := by simp
+lemma of_real_mul' (r : ℝ) (z : ℂ) : (↑r * z) = ⟨r * z.re, r * z.im⟩ :=
+ext (of_real_mul_re _ _) (of_real_mul_im _ _)
 
 /-! ### The imaginary unit, `I` -/
 

src/data/complex/is_R_or_C.lean

@@ -146,20 +146,17 @@ ext_iff.2 $ by simp
 ext_iff.2 $ by simp
 lemma of_real_mul_re (r : ℝ) (z : K) : re (↑r * z) = r * re z :=
 by simp only [mul_re, of_real_im, zero_mul, of_real_re, sub_zero]
-
-lemma smul_re (r : ℝ) (z : K) : re (↑r * z) = r * (re z) :=
-by simp only [of_real_im, zero_mul, of_real_re, sub_zero, mul_re]
-lemma smul_im (r : ℝ) (z : K) : im (↑r * z) = r * (im z) :=
+lemma of_real_mul_im (r : ℝ) (z : K) : im (↑r * z) = r * (im z) :=
 by simp only [add_zero, of_real_im, zero_mul, of_real_re, mul_im]
 
-lemma smul_re' : ∀ (r : ℝ) (z : K), re (r • z) = r * (re z) :=
-λ r z, by { rw algebra.smul_def, apply smul_re }
-lemma smul_im' : ∀ (r : ℝ) (z : K), im (r • z) = r * (im z) :=
-λ r z, by { rw algebra.smul_def, apply smul_im }
+lemma smul_re : ∀ (r : ℝ) (z : K), re (r • z) = r * (re z) :=
+λ r z, by { rw algebra.smul_def, apply of_real_mul_re }
+lemma smul_im : ∀ (r : ℝ) (z : K), im (r • z) = r * (im z) :=
+λ r z, by { rw algebra.smul_def, apply of_real_mul_im }
 
 /-- The real part in a `is_R_or_C` field, as a linear map. -/
 noncomputable def re_lm : K →ₗ[ℝ] ℝ :=
-{ map_smul' := smul_re',  .. re }
+{ map_smul' := smul_re,  .. re }
 
 @[simp] lemma re_lm_coe : (re_lm : K → ℝ) = re := rfl
 

src/data/complex/module.lean

@@ -12,10 +12,12 @@ import linear_algebra.finite_dimensional
 /-!
 # Complex number as a vector space over `ℝ`
 
-This file contains three instances:
-* `ℂ` is an `ℝ` algebra;
+This file contains the following instances:
+* Any `•`-structure (`has_scalar`, `mul_action`, `distrib_mul_action`, `semimodule`, `algebra`) on
+  `ℝ` imbues a corresponding structure on `ℂ`. This includes the statement that `ℂ` is an `ℝ`
+  algebra.
 * any complex vector space is a real vector space;
-* any finite dimensional complex vector space is a finite dimesional real vector space;
+* any finite dimensional complex vector space is a finite dimensional real vector space;
 * the space of `ℝ`-linear maps from a real vector space to a complex vector space is a complex
   vector space.
 
@@ -32,9 +34,47 @@ noncomputable theory
 
 namespace complex
 
-instance algebra_over_reals : algebra ℝ ℂ := (complex.of_real).to_algebra
+variables {R : Type*} {S : Type*}
 
-@[simp] lemma smul_coe {x : ℝ} {z : ℂ} : x • z = x * z := rfl
+section
+
+variables [has_scalar R ℝ]
+
+instance : has_scalar R ℂ :=
+{ smul := λ r x, ⟨r • x.re, r • x.im⟩ }
+
+lemma smul_re (r : R) (z : ℂ) : (r • z).re = r • z.re := rfl
+lemma smul_im (r : R) (z : ℂ) : (r • z).im = r • z.im := rfl
+
+@[simp] lemma smul_coe {x : ℝ} {z : ℂ} : x • z = x * z :=
+by ext; simp [smul_re, smul_im]
+
+end
+
+instance [has_scalar R ℝ] [has_scalar S ℝ] [smul_comm_class R S ℝ] : smul_comm_class R S ℂ :=
+{ smul_comm := λ r s x, ext (smul_comm _ _ _) (smul_comm _ _ _) }
+
+instance [has_scalar R S] [has_scalar R ℝ] [has_scalar S ℝ] [is_scalar_tower R S ℝ] :
+  is_scalar_tower R S ℂ :=
+{ smul_assoc := λ r s x, ext (smul_assoc _ _ _) (smul_assoc _ _ _) }
+
+instance [monoid R] [mul_action R ℝ] : mul_action R ℂ :=
+{ one_smul := λ x, ext (one_smul _ _) (one_smul _ _),
+  mul_smul := λ r s x, ext (mul_smul _ _ _) (mul_smul _ _ _) }
+
+instance [semiring R] [distrib_mul_action R ℝ] : distrib_mul_action R ℂ :=
+{ smul_add := λ r x y, ext (smul_add _ _ _) (smul_add _ _ _),
+  smul_zero := λ r, ext (smul_zero _) (smul_zero _) }
+
+instance [semiring R] [semimodule R ℝ] : semimodule R ℂ :=
+{ add_smul := λ r s x, ext (add_smul _ _ _) (add_smul _ _ _),
+  zero_smul := λ r, ext (zero_smul _ _) (zero_smul _ _) }
+
+instance [comm_semiring R] [algebra R ℝ] : algebra R ℂ :=
+{ smul := (•),
+  smul_def' := λ r x, by ext; simp [smul_re, smul_im, algebra.smul_def],
+  commutes' := λ r ⟨xr, xi⟩, by ext; simp [smul_re, smul_im, algebra.commutes],
+  ..complex.of_real.comp (algebra_map R ℝ) }
 
 section
 open_locale complex_order

src/ring_theory/polynomial/cyclotomic.lean

@@ -688,7 +688,8 @@ lemma cyclotomic.irreducible {n : ℕ} (hpos : 0 < n) : irreducible (cyclotomic
 begin
   have h0 := (ne_of_lt hpos).symm,
   rw [cyclotomic_eq_minpoly (is_primitive_root_exp n h0) hpos],
-  exact minpoly.irreducible (is_integral (is_primitive_root_exp n h0) hpos)
+  apply minpoly.irreducible,
+  exact (is_primitive_root_exp n h0).is_integral hpos,
 end
 
 end minpoly