[Merged by Bors] - refactor(Analysis/NormedSpace/Exponential): remove the 𝕂 argument from exp

Mathlib/Analysis/CStarAlgebra/Exponential.lean

@@ -31,8 +31,9 @@ open Complex
 over ℂ. -/
 @[simps]
 noncomputable def selfAdjoint.expUnitary (a : selfAdjoint A) : unitary A :=
-  ⟨exp ℂ ((I • a.val) : A),
-      exp_mem_unitary_of_mem_skewAdjoint _ (a.prop.smul_mem_skewAdjoint conj_I)⟩
+  ⟨exp ((I • a.val) : A),
+      have : NormedAlgebra ℚ A := .restrictScalars ℚ ℂ A
+      exp_mem_unitary_of_mem_skewAdjoint (a.prop.smul_mem_skewAdjoint conj_I)⟩
 
 open selfAdjoint
 
@@ -44,10 +45,12 @@ lemma selfAdjoint.expUnitary_zero : expUnitary (0 : selfAdjoint A) = 1 := by
 @[fun_prop]
 lemma selfAdjoint.continuous_expUnitary : Continuous (expUnitary : selfAdjoint A → unitary A) := by
   simp only [continuous_induced_rng, Function.comp_def, selfAdjoint.expUnitary_coe]
+  have : NormedAlgebra ℚ A := NormedAlgebra.restrictScalars ℚ ℂ A
   fun_prop
 
 theorem Commute.expUnitary_add {a b : selfAdjoint A} (h : Commute (a : A) (b : A)) :
     expUnitary (a + b) = expUnitary a * expUnitary b := by
+  have : NormedAlgebra ℚ A := .restrictScalars ℚ ℂ A
   ext
   have hcomm : Commute (I • (a : A)) (I • (b : A)) := by
     unfold Commute SemiconjBy

Mathlib/Analysis/CStarAlgebra/Spectrum.lean

@@ -150,9 +150,10 @@ variable [StarModule ℂ A]
 /-- Any element of the spectrum of a selfadjoint is real. -/
 theorem IsSelfAdjoint.mem_spectrum_eq_re {a : A} (ha : IsSelfAdjoint a) {z : ℂ}
     (hz : z ∈ spectrum ℂ a) : z = z.re := by
-  have hu := exp_mem_unitary_of_mem_skewAdjoint ℂ (ha.smul_mem_skewAdjoint conj_I)
+  have : NormedAlgebra ℚ A := .restrictScalars ℚ ℂ A
+  have hu := exp_mem_unitary_of_mem_skewAdjoint (ha.smul_mem_skewAdjoint conj_I)
   let Iu := Units.mk0 I I_ne_zero
-  have : NormedSpace.exp ℂ (I • z) ∈ spectrum ℂ (NormedSpace.exp ℂ (I • a)) := by
+  have : NormedSpace.exp (I • z) ∈ spectrum ℂ (NormedSpace.exp (I • a)) := by
     simpa only [Units.smul_def, Units.val_mk0] using
       spectrum.exp_mem_exp (Iu • a) (smul_mem_smul_iff.mpr hz)
   exact Complex.ext (ofReal_re _) <| by

Mathlib/Analysis/CStarAlgebra/Unitary/Connected.lean

@@ -136,7 +136,7 @@ lemma selfAdjoint.norm_sq_expUnitary_sub_one {x : selfAdjoint A} (hx : ‖x‖ 
   nontriviality A
   apply norm_sub_one_sq_eq (expUnitary x).2
   simp only [expUnitary_coe, AddSubgroupClass.coe_norm]
-  rw [← CFC.exp_eq_normedSpace_exp, ← cfc_comp_smul I _ (x : A), cfc_map_spectrum ..,
+  rw [← CFC.exp_eq_normedSpace_exp (𝕜 := ℂ), ← cfc_comp_smul I _ (x : A), cfc_map_spectrum ..,
     ← x.2.spectrumRestricts.algebraMap_image]
   simp only [Set.image_image, coe_algebraMap, smul_eq_mul, mul_comm I, ← exp_eq_exp_ℂ,
     exp_ofReal_mul_I_re]
@@ -161,10 +161,10 @@ lemma argSelfAdjoint_expUnitary {x : selfAdjoint A} (hx : ‖x‖ < π) :
         exact Real.cos_lt_cos_of_nonneg_of_le_pi (by positivity) le_rfl hx
       _ = 2 ^ 2 := by norm_num
   simp only [argSelfAdjoint_coe, expUnitary_coe]
-  rw [← CFC.exp_eq_normedSpace_exp, ← cfc_comp_smul .., ← cfc_comp' (hg := ?hg)]
+  rw [← CFC.exp_eq_normedSpace_exp (𝕜 := ℂ), ← cfc_comp_smul .., ← cfc_comp' (hg := ?hg)]
   case hg =>
     refine continuous_ofReal.comp_continuousOn <| continuousOn_arg.mono ?_
-    rwa [expUnitary_coe, ← CFC.exp_eq_normedSpace_exp, ← cfc_comp_smul ..,
+    rwa [expUnitary_coe, ← CFC.exp_eq_normedSpace_exp (𝕜 := ℂ), ← cfc_comp_smul ..,
       cfc_map_spectrum ..] at this
   conv_rhs => rw [← cfc_id' ℂ (x : A)]
   refine cfc_congr fun y hy ↦ ?_
@@ -180,7 +180,7 @@ lemma expUnitary_argSelfAdjoint {u : unitary A} (hu : ‖(u - 1 : A)‖ < 2) :
   ext
   have : ContinuousOn arg (spectrum ℂ (u : A)) :=
     continuousOn_arg.mono <| (spectrum_subset_slitPlane_iff_norm_lt_two u.2).mpr hu
-  rw [expUnitary_coe, argSelfAdjoint_coe, ← CFC.exp_eq_normedSpace_exp,
+  rw [expUnitary_coe, argSelfAdjoint_coe, ← CFC.exp_eq_normedSpace_exp (𝕜 := ℂ),
     ← cfc_comp_smul .., ← cfc_comp' ..]
   conv_rhs => rw [← cfc_id' ℂ (u : A)]
   refine cfc_congr fun y hy ↦ ?_

Mathlib/Analysis/Normed/Algebra/DualNumber.lean

@@ -23,16 +23,16 @@ namespace DualNumber
 
 open TrivSqZeroExt
 
-variable (𝕜 : Type*) {R : Type*}
-variable [Field 𝕜] [CharZero 𝕜] [CommRing R] [Algebra 𝕜 R]
+variable {R : Type*}
+variable [CommRing R] [Algebra ℚ R]
 variable [UniformSpace R] [IsTopologicalRing R] [T2Space R]
 
 @[simp]
-theorem exp_eps : exp 𝕜 (eps : DualNumber R) = 1 + eps :=
-  exp_inr _ _
+theorem exp_eps : exp (eps : DualNumber R) = 1 + eps :=
+  exp_inr _
 
 @[simp]
-theorem exp_smul_eps (r : R) : exp 𝕜 (r • eps : DualNumber R) = 1 + r • eps := by
+theorem exp_smul_eps (r : R) : exp (r • eps : DualNumber R) = 1 + r • eps := by
   rw [eps, ← inr_smul, exp_inr]
 
 end DualNumber