From 9c7f0987f54d8e82cfc7aca40f1dce28e4537de3 Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Fri, 6 May 2022 20:44:01 +0000
Subject: [PATCH 1/6] =?UTF-8?q?feat(analysis/normed=5Fspace/exponential):?=
 =?UTF-8?q?=20Generalize=20`field`=20lemmas=20about=20`exp=20=F0=9D=95=82?=
 =?UTF-8?q?=20=F0=9D=95=82`=20to=20`division=5Fring`=20lemmas=20about=20`e?=
 =?UTF-8?q?xp=20=F0=9D=95=82=20=F0=9D=94=B8`?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

All of these lemmas are true when `𝕂` and `𝔸` are different; all we require is that `𝔸` is a `division_ring`.

This moves the lemmas down to the appropriate division_ring sections, and replaces the word `field` with `div` in their names.
---
 src/analysis/normed_space/exponential.lean    | 112 ++++++++++--------
 .../special_functions/exponential.lean        |   6 +-
 src/analysis/specific_limits/normed.lean      |   2 +-
 .../derangements/exponential.lean             |   2 +-
 4 files changed, 66 insertions(+), 56 deletions(-)

diff --git a/src/analysis/normed_space/exponential.lean b/src/analysis/normed_space/exponential.lean
index 1b5d2544146c7..735ad0aa1b88b 100644
--- a/src/analysis/normed_space/exponential.lean
+++ b/src/analysis/normed_space/exponential.lean
@@ -88,31 +88,13 @@ lemma exp_series_apply_eq' (x : 𝔸) :
   (λ n, exp_series 𝕂 𝔸 n (λ _, x)) = (λ n, (n!⁻¹ : 𝕂) • x^n) :=
 funext (exp_series_apply_eq x)
 
-lemma exp_series_apply_eq_field [topological_space 𝕂] [topological_ring 𝕂] (x : 𝕂) (n : ℕ) :
-  exp_series 𝕂 𝕂 n (λ _, x) = x^n / n! :=
-begin
-  rw [div_eq_inv_mul, ←smul_eq_mul],
-  exact exp_series_apply_eq x n,
-end
-
-lemma exp_series_apply_eq_field' [topological_space 𝕂] [topological_ring 𝕂] (x : 𝕂) :
-  (λ n, exp_series 𝕂 𝕂 n (λ _, x)) = (λ n, x^n / n!) :=
-funext (exp_series_apply_eq_field x)
-
 lemma exp_series_sum_eq (x : 𝔸) : (exp_series 𝕂 𝔸).sum x = ∑' (n : ℕ), (n!⁻¹ : 𝕂) • x^n :=
 tsum_congr (λ n, exp_series_apply_eq x n)
 
-lemma exp_series_sum_eq_field [topological_space 𝕂] [topological_ring 𝕂] (x : 𝕂) :
-  (exp_series 𝕂 𝕂).sum x = ∑' (n : ℕ), x^n / n! :=
-tsum_congr (λ n, exp_series_apply_eq_field x n)
 
 lemma exp_eq_tsum : exp 𝕂 = (λ x : 𝔸, ∑' (n : ℕ), (n!⁻¹ : 𝕂) • x^n) :=
 funext exp_series_sum_eq
 
-lemma exp_eq_tsum_field [topological_space 𝕂] [topological_ring 𝕂] :
-  exp 𝕂 = (λ x : 𝕂, ∑' (n : ℕ), x^n / n!) :=
-funext exp_series_sum_eq_field
-
 @[simp] lemma exp_zero [t2_space 𝔸] : exp 𝕂 (0 : 𝔸) = 1 :=
 begin
   suffices : (λ x : 𝔸, ∑' (n : ℕ), (n!⁻¹ : 𝕂) • x^n) 0 = ∑' (n : ℕ), if n = 0 then 1 else 0,
@@ -141,6 +123,25 @@ lemma commute.exp [t2_space 𝔸] {x y : 𝔸} (h : commute x y) : commute (exp
 
 end topological_algebra
 
+section topological_division_algebra
+variables {𝕂 𝔸 : Type*} [field 𝕂] [division_ring 𝔸] [algebra 𝕂 𝔸] [topological_space 𝔸]
+  [topological_ring 𝔸]
+
+lemma exp_series_apply_eq_div (x : 𝔸) (n : ℕ) : exp_series 𝕂 𝔸 n (λ _, x) = x^n / n! :=
+by rw [div_eq_mul_inv, ←(nat.cast_commute n! (x ^ n)).inv_left₀.eq, ←smul_eq_mul,
+    exp_series_apply_eq, inv_nat_cast_smul_eq _ _ _ _]
+
+lemma exp_series_apply_eq_div' (x : 𝔸) : (λ n, exp_series 𝕂 𝔸 n (λ _, x)) = (λ n, x^n / n!) :=
+funext (exp_series_apply_eq_div x)
+
+lemma exp_series_sum_eq_div (x : 𝔸) : (exp_series 𝕂 𝔸).sum x = ∑' (n : ℕ), x^n / n! :=
+tsum_congr (exp_series_apply_eq_div x)
+
+lemma exp_eq_tsum_div : exp 𝕂 = (λ x : 𝔸, ∑' (n : ℕ), x^n / n!) :=
+funext exp_series_sum_eq_div
+
+end topological_division_algebra
+
 section normed
 
 section any_field_any_algebra
@@ -162,15 +163,6 @@ begin
   exact norm_exp_series_summable_of_mem_ball x hx
 end
 
-lemma norm_exp_series_field_summable_of_mem_ball (x : 𝕂)
-  (hx : x ∈ emetric.ball (0 : 𝕂) (exp_series 𝕂 𝕂).radius) :
-  summable (λ n, ∥x^n / n!∥) :=
-begin
-  change summable (norm ∘ _),
-  rw ← exp_series_apply_eq_field',
-  exact norm_exp_series_summable_of_mem_ball x hx
-end
-
 section complete_algebra
 
 variables [complete_space 𝔸]
@@ -185,10 +177,6 @@ lemma exp_series_summable_of_mem_ball' (x : 𝔸)
   summable (λ n, (n!⁻¹ : 𝕂) • x^n) :=
 summable_of_summable_norm (norm_exp_series_summable_of_mem_ball' x hx)
 
-lemma exp_series_field_summable_of_mem_ball [complete_space 𝕂] (x : 𝕂)
-  (hx : x ∈ emetric.ball (0 : 𝕂) (exp_series 𝕂 𝕂).radius) : summable (λ n, x^n / n!) :=
-summable_of_summable_norm (norm_exp_series_field_summable_of_mem_ball x hx)
-
 lemma exp_series_has_sum_exp_of_mem_ball (x : 𝔸)
   (hx : x ∈ emetric.ball (0 : 𝔸) (exp_series 𝕂 𝔸).radius) :
   has_sum (λ n, exp_series 𝕂 𝔸 n (λ _, x)) (exp 𝕂 x) :=
@@ -202,13 +190,6 @@ begin
   exact exp_series_has_sum_exp_of_mem_ball x hx
 end
 
-lemma exp_series_field_has_sum_exp_of_mem_ball [complete_space 𝕂] (x : 𝕂)
-  (hx : x ∈ emetric.ball (0 : 𝕂) (exp_series 𝕂 𝕂).radius) : has_sum (λ n, x^n / n!) (exp 𝕂 x) :=
-begin
-  rw ← exp_series_apply_eq_field',
-  exact exp_series_has_sum_exp_of_mem_ball x hx
-end
-
 lemma has_fpower_series_on_ball_exp_of_radius_pos (h : 0 < (exp_series 𝕂 𝔸).radius) :
   has_fpower_series_on_ball (exp 𝕂) (exp_series 𝕂 𝔸) 0 (exp_series 𝕂 𝔸).radius :=
 (exp_series 𝕂 𝔸).has_fpower_series_on_ball h
@@ -301,6 +282,30 @@ section any_field_division_algebra
 
 variables {𝕂 𝔸 : Type*} [nondiscrete_normed_field 𝕂] [normed_division_ring 𝔸] [normed_algebra 𝕂 𝔸]
 
+variables (𝕂)
+
+lemma norm_exp_series_div_summable_of_mem_ball (x : 𝔸)
+  (hx : x ∈ emetric.ball (0 : 𝔸) (exp_series 𝕂 𝔸).radius) :
+  summable (λ n, ∥x^n / n!∥) :=
+begin
+  change summable (norm ∘ _),
+  rw ← exp_series_apply_eq_div' x,
+  exact norm_exp_series_summable_of_mem_ball x hx
+end
+
+lemma exp_series_div_summable_of_mem_ball [complete_space 𝔸] (x : 𝔸)
+  (hx : x ∈ emetric.ball (0 : 𝔸) (exp_series 𝕂 𝔸).radius) : summable (λ n, x^n / n!) :=
+summable_of_summable_norm (norm_exp_series_div_summable_of_mem_ball 𝕂 x hx)
+
+lemma exp_series_div_has_sum_exp_of_mem_ball [complete_space 𝔸] (x : 𝔸)
+  (hx : x ∈ emetric.ball (0 : 𝔸) (exp_series 𝕂 𝔸).radius) : has_sum (λ n, x^n / n!) (exp 𝕂 x) :=
+begin
+  rw ← exp_series_apply_eq_div' x,
+  exact exp_series_has_sum_exp_of_mem_ball x hx
+end
+
+variables {𝕂}
+
 lemma exp_neg_of_mem_ball [char_zero 𝕂] [complete_space 𝔸] {x : 𝔸}
   (hx : x ∈ emetric.ball (0 : 𝔸) (exp_series 𝕂 𝔸).radius) :
   exp 𝕂 (-x) = (exp 𝕂 x)⁻¹ :=
@@ -356,17 +361,13 @@ end
 
 variables {𝕂 𝔸 𝔹}
 
-section complete_algebra
-
 lemma norm_exp_series_summable (x : 𝔸) : summable (λ n, ∥exp_series 𝕂 𝔸 n (λ _, x)∥) :=
 norm_exp_series_summable_of_mem_ball x ((exp_series_radius_eq_top 𝕂 𝔸).symm ▸ edist_lt_top _ _)
 
 lemma norm_exp_series_summable' (x : 𝔸) : summable (λ n, ∥(n!⁻¹ : 𝕂) • x^n∥) :=
 norm_exp_series_summable_of_mem_ball' x ((exp_series_radius_eq_top 𝕂 𝔸).symm ▸ edist_lt_top _ _)
 
-lemma norm_exp_series_field_summable (x : 𝕂) : summable (λ n, ∥x^n / n!∥) :=
-norm_exp_series_field_summable_of_mem_ball x
-  ((exp_series_radius_eq_top 𝕂 𝕂).symm ▸ edist_lt_top _ _)
+section complete_algebra
 
 variables [complete_space 𝔸]
 
@@ -376,18 +377,12 @@ summable_of_summable_norm (norm_exp_series_summable x)
 lemma exp_series_summable' (x : 𝔸) : summable (λ n, (n!⁻¹ : 𝕂) • x^n) :=
 summable_of_summable_norm (norm_exp_series_summable' x)
 
-lemma exp_series_field_summable (x : 𝕂) : summable (λ n, x^n / n!) :=
-summable_of_summable_norm (norm_exp_series_field_summable x)
-
 lemma exp_series_has_sum_exp (x : 𝔸) : has_sum (λ n, exp_series 𝕂 𝔸 n (λ _, x)) (exp 𝕂 x) :=
 exp_series_has_sum_exp_of_mem_ball x ((exp_series_radius_eq_top 𝕂 𝔸).symm ▸ edist_lt_top _ _)
 
 lemma exp_series_has_sum_exp' (x : 𝔸) : has_sum (λ n, (n!⁻¹ : 𝕂) • x^n) (exp 𝕂 x):=
 exp_series_has_sum_exp_of_mem_ball' x ((exp_series_radius_eq_top 𝕂 𝔸).symm ▸ edist_lt_top _ _)
 
-lemma exp_series_field_has_sum_exp (x : 𝕂) : has_sum (λ n, x^n / n!) (exp 𝕂 x):=
-exp_series_field_has_sum_exp_of_mem_ball x ((exp_series_radius_eq_top 𝕂 𝕂).symm ▸ edist_lt_top _ _)
-
 lemma exp_has_fpower_series_on_ball :
   has_fpower_series_on_ball (exp 𝕂) (exp_series 𝕂 𝔸) 0 ∞ :=
 exp_series_radius_eq_top 𝕂 𝔸 ▸
@@ -397,8 +392,7 @@ lemma exp_has_fpower_series_at_zero :
   has_fpower_series_at (exp 𝕂) (exp_series 𝕂 𝔸) 0 :=
 exp_has_fpower_series_on_ball.has_fpower_series_at
 
-lemma exp_continuous :
-  continuous (exp 𝕂 : 𝔸 → 𝔸) :=
+lemma exp_continuous : continuous (exp 𝕂 : 𝔸 → 𝔸) :=
 begin
   rw [continuous_iff_continuous_on_univ, ← metric.eball_top_eq_univ (0 : 𝔸),
       ← exp_series_radius_eq_top 𝕂 𝔸],
@@ -528,8 +522,24 @@ end any_algebra
 section division_algebra
 
 variables {𝕂 𝔸 : Type*} [is_R_or_C 𝕂] [normed_division_ring 𝔸] [normed_algebra 𝕂 𝔸]
+
+variables (𝕂)
+
+lemma norm_exp_series_div_summable (x : 𝔸) : summable (λ n, ∥x^n / n!∥) :=
+norm_exp_series_div_summable_of_mem_ball 𝕂 x
+  ((exp_series_radius_eq_top 𝕂 𝔸).symm ▸ edist_lt_top _ _)
+
 variables [complete_space 𝔸]
 
+lemma exp_series_div_summable (x : 𝔸) : summable (λ n, x^n / n!) :=
+summable_of_summable_norm (norm_exp_series_div_summable 𝕂 x)
+
+lemma exp_series_div_has_sum_exp (x : 𝔸) : has_sum (λ n, x^n / n!) (exp 𝕂 x):=
+exp_series_div_has_sum_exp_of_mem_ball 𝕂 x
+  ((exp_series_radius_eq_top 𝕂 𝔸).symm ▸ edist_lt_top _ _)
+
+variables {𝕂}
+
 lemma exp_neg (x : 𝔸) : exp 𝕂 (-x) = (exp 𝕂 x)⁻¹ :=
 exp_neg_of_mem_ball $ (exp_series_radius_eq_top 𝕂 𝔸).symm ▸ edist_lt_top _ _
 
diff --git a/src/analysis/special_functions/exponential.lean b/src/analysis/special_functions/exponential.lean
index 4e7e63ad2e68a..7d4ffb38ec4fd 100644
--- a/src/analysis/special_functions/exponential.lean
+++ b/src/analysis/special_functions/exponential.lean
@@ -207,9 +207,9 @@ section complex
 lemma complex.exp_eq_exp_ℂ : complex.exp = exp ℂ :=
 begin
   refine funext (λ x, _),
-  rw [complex.exp, exp_eq_tsum_field],
+  rw [complex.exp, exp_eq_tsum_div],
   exact tendsto_nhds_unique x.exp'.tendsto_limit
-    (exp_series_field_summable x).has_sum.tendsto_sum_nat
+    (exp_series_div_summable ℝ x).has_sum.tendsto_sum_nat
 end
 
 end complex
@@ -219,7 +219,7 @@ section real
 lemma real.exp_eq_exp_ℝ : real.exp = exp ℝ :=
 begin
   refine funext (λ x, _),
-  rw [real.exp, complex.exp_eq_exp_ℂ, ← exp_ℝ_ℂ_eq_exp_ℂ_ℂ, exp_eq_tsum, exp_eq_tsum_field,
+  rw [real.exp, complex.exp_eq_exp_ℂ, ← exp_ℝ_ℂ_eq_exp_ℂ_ℂ, exp_eq_tsum, exp_eq_tsum_div,
       ← re_to_complex, ← re_clm_apply, re_clm.map_tsum (exp_series_summable' (x : ℂ))],
   refine tsum_congr (λ n, _),
   rw [re_clm.map_smul, ← complex.of_real_pow, re_clm_apply, re_to_complex, complex.of_real_re,
diff --git a/src/analysis/specific_limits/normed.lean b/src/analysis/specific_limits/normed.lean
index bb546303e235d..d4262585172aa 100644
--- a/src/analysis/specific_limits/normed.lean
+++ b/src/analysis/specific_limits/normed.lean
@@ -622,7 +622,7 @@ end
 ### Factorial
 -/
 
-/-- The series `∑' n, x ^ n / n!` is summable of any `x : ℝ`. See also `exp_series_field_summable`
+/-- The series `∑' n, x ^ n / n!` is summable of any `x : ℝ`. See also `exp_series_div_summable`
 for a version that also works in `ℂ`, and `exp_series_summable'` for a version that works in
 any normed algebra over `ℝ` or `ℂ`. -/
 lemma real.summable_pow_div_factorial (x : ℝ) :
diff --git a/src/combinatorics/derangements/exponential.lean b/src/combinatorics/derangements/exponential.lean
index 3240daf71c8f2..f6804d70080fd 100644
--- a/src/combinatorics/derangements/exponential.lean
+++ b/src/combinatorics/derangements/exponential.lean
@@ -35,7 +35,7 @@ begin
     -- there's no specific lemma for ℝ that ∑ x^k/k! sums to exp(x), but it's
     -- true in more general fields, so use that lemma
     rw real.exp_eq_exp_ℝ,
-    exact exp_series_field_has_sum_exp (-1 : ℝ) },
+    exact exp_series_div_has_sum_exp (-1 : ℝ) },
   intro n,
   rw [← int.cast_coe_nat, num_derangements_sum],
   push_cast,

From 48fc050b74fc4cb93df9fc6e76f0b09d5cd8f9d8 Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Fri, 6 May 2022 20:47:35 +0000
Subject: [PATCH 2/6] authorship

---
 src/analysis/normed_space/exponential.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/analysis/normed_space/exponential.lean b/src/analysis/normed_space/exponential.lean
index 735ad0aa1b88b..f3b4c562d19f2 100644
--- a/src/analysis/normed_space/exponential.lean
+++ b/src/analysis/normed_space/exponential.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2021 Anatole Dedecker. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Anatole Dedecker
+Authors: Anatole Dedecker, Eric Wieser
 -/
 import analysis.specific_limits.basic
 import analysis.analytic.basic

From fc42704ccabed587fc135b7a5a1680643281a1a5 Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Fri, 6 May 2022 20:48:45 +0000
Subject: [PATCH 3/6] fix blank line

---
 src/analysis/normed_space/exponential.lean | 1 -
 1 file changed, 1 deletion(-)

diff --git a/src/analysis/normed_space/exponential.lean b/src/analysis/normed_space/exponential.lean
index f3b4c562d19f2..8871437bbde33 100644
--- a/src/analysis/normed_space/exponential.lean
+++ b/src/analysis/normed_space/exponential.lean
@@ -91,7 +91,6 @@ funext (exp_series_apply_eq x)
 lemma exp_series_sum_eq (x : 𝔸) : (exp_series 𝕂 𝔸).sum x = ∑' (n : ℕ), (n!⁻¹ : 𝕂) • x^n :=
 tsum_congr (λ n, exp_series_apply_eq x n)
 
-
 lemma exp_eq_tsum : exp 𝕂 = (λ x : 𝔸, ∑' (n : ℕ), (n!⁻¹ : 𝕂) • x^n) :=
 funext exp_series_sum_eq
 

From bcc9e98bafb5e92b4b0b5b4548a2856b206f2679 Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Fri, 6 May 2022 21:25:44 +0000
Subject: [PATCH 4/6] fix

---
 src/combinatorics/derangements/exponential.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/combinatorics/derangements/exponential.lean b/src/combinatorics/derangements/exponential.lean
index f6804d70080fd..afd91585d11dd 100644
--- a/src/combinatorics/derangements/exponential.lean
+++ b/src/combinatorics/derangements/exponential.lean
@@ -35,7 +35,7 @@ begin
     -- there's no specific lemma for ℝ that ∑ x^k/k! sums to exp(x), but it's
     -- true in more general fields, so use that lemma
     rw real.exp_eq_exp_ℝ,
-    exact exp_series_div_has_sum_exp (-1 : ℝ) },
+    exact exp_series_div_has_sum_exp ℝ (-1 : ℝ) },
   intro n,
   rw [← int.cast_coe_nat, num_derangements_sum],
   push_cast,

From a4558132393ffaaa65e2e61db7accdf03a35420a Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Fri, 6 May 2022 23:23:50 +0000
Subject: [PATCH 5/6] wip

---
 src/analysis/normed_space/exponential.lean | 242 +++++++++++----------
 1 file changed, 126 insertions(+), 116 deletions(-)

diff --git a/src/analysis/normed_space/exponential.lean b/src/analysis/normed_space/exponential.lean
index 8871437bbde33..97ccaf0a60960 100644
--- a/src/analysis/normed_space/exponential.lean
+++ b/src/analysis/normed_space/exponential.lean
@@ -12,7 +12,7 @@ import data.finset.noncomm_prod
 /-!
 # Exponential in a Banach algebra
 
-In this file, we define `exp 𝕂 : 𝔸 → 𝔸`, the exponential map in a topological algebra `𝔸` over a
+In this file, we define `exp : 𝔸 → 𝔸`, the exponential map in a topological algebra `𝔸` over a
 field `𝕂`.
 
 While for most interesting results we need `𝔸` to be normed algebra, we do not require this in the
@@ -31,22 +31,22 @@ We prove most result for an arbitrary field `𝕂`, and then specialize to `𝕂
 
 - `exp_add_of_commute_of_mem_ball` : if `𝕂` has characteristic zero, then given two commuting
   elements `x` and `y` in the disk of convergence, we have
-  `exp 𝕂 (x+y) = (exp 𝕂 x) * (exp 𝕂 y)`
+  `exp (x+y) = (exp x) * (exp y)`
 - `exp_add_of_mem_ball` : if `𝕂` has characteristic zero and `𝔸` is commutative, then given two
   elements `x` and `y` in the disk of convergence, we have
-  `exp 𝕂 (x+y) = (exp 𝕂 x) * (exp 𝕂 y)`
+  `exp (x+y) = (exp x) * (exp y)`
 - `exp_neg_of_mem_ball` : if `𝕂` has characteristic zero and `𝔸` is a division ring, then given an
-  element `x` in the disk of convergence, we have `exp 𝕂 (-x) = (exp 𝕂 x)⁻¹`.
+  element `x` in the disk of convergence, we have `exp (-x) = (exp x)⁻¹`.
 
 ### `𝕂 = ℝ` or `𝕂 = ℂ`
 
-- `exp_series_radius_eq_top` : the `formal_multilinear_series` defining `exp 𝕂` has infinite
+- `exp_series_radius_eq_top` : the `formal_multilinear_series` defining `exp` has infinite
   radius of convergence
 - `exp_add_of_commute` : given two commuting elements `x` and `y`, we have
-  `exp 𝕂 (x+y) = (exp 𝕂 x) * (exp 𝕂 y)`
-- `exp_add` : if `𝔸` is commutative, then we have `exp 𝕂 (x+y) = (exp 𝕂 x) * (exp 𝕂 y)`
+  `exp (x+y) = (exp x) * (exp y)`
+- `exp_add` : if `𝔸` is commutative, then we have `exp (x+y) = (exp x) * (exp y)`
   for any `x` and `y`
-- `exp_neg` : if `𝔸` is a division ring, then we have `exp 𝕂 (-x) = (exp 𝕂 x)⁻¹`.
+- `exp_neg` : if `𝔸` is a division ring, then we have `exp (-x) = (exp x)⁻¹`.
 - `exp_sum_of_commute` : the analogous result to `exp_add_of_commute` for `finset.sum`.
 - `exp_sum` : the analogous result to `exp_add` for `finset.sum`.
 - `exp_nsmul` : repeated addition in the domain corresponds to repeated multiplication in the
@@ -56,7 +56,7 @@ We prove most result for an arbitrary field `𝕂`, and then specialize to `𝕂
 
 ### Other useful compatibility results
 
-- `exp_eq_exp` : if `𝔸` is a normed algebra over two fields `𝕂` and `𝕂'`, then `exp 𝕂 = exp 𝕂' 𝔸`
+- `exp_eq_exp` : if `𝔸` is a normed algebra over two fields `𝕂` and `𝕂'`, then `exp = exp' 𝔸`
 
 -/
 
@@ -69,15 +69,15 @@ variables (𝕂 𝔸 : Type*) [field 𝕂] [ring 𝔸] [algebra 𝕂 𝔸] [topo
   [topological_ring 𝔸]
 
 /-- `exp_series 𝕂 𝔸` is the `formal_multilinear_series` whose `n`-th term is the map
-`(xᵢ) : 𝔸ⁿ ↦ (1/n! : 𝕂) • ∏ xᵢ`. Its sum is the exponential map `exp 𝕂 : 𝔸 → 𝔸`. -/
+`(xᵢ) : 𝔸ⁿ ↦ (1/n! : 𝕂) • ∏ xᵢ`. Its sum is the exponential map `exp : 𝔸 → 𝔸`. -/
 def exp_series : formal_multilinear_series 𝕂 𝔸 𝔸 :=
 λ n, (n!⁻¹ : 𝕂) • continuous_multilinear_map.mk_pi_algebra_fin 𝕂 n 𝔸
 
 variables {𝔸}
 
-/-- `exp 𝕂 : 𝔸 → 𝔸` is the exponential map determined by the action of `𝕂` on `𝔸`.
+/-- `exp : 𝔸 → 𝔸` is the exponential map determined by the action of `𝕂` on `𝔸`.
 It is defined as the sum of the `formal_multilinear_series` `exp_series 𝕂 𝔸`. -/
-noncomputable def exp (x : 𝔸) : 𝔸 := (exp_series 𝕂 𝔸).sum x
+noncomputable def exp [algebra ℚ 𝔸] (x : 𝔸) : 𝔸 := (exp_series ℚ 𝔸).sum x
 
 variables {𝕂 𝔸}
 
@@ -91,12 +91,20 @@ funext (exp_series_apply_eq x)
 lemma exp_series_sum_eq (x : 𝔸) : (exp_series 𝕂 𝔸).sum x = ∑' (n : ℕ), (n!⁻¹ : 𝕂) • x^n :=
 tsum_congr (λ n, exp_series_apply_eq x n)
 
-lemma exp_eq_tsum : exp 𝕂 = (λ x : 𝔸, ∑' (n : ℕ), (n!⁻¹ : 𝕂) • x^n) :=
+lemma exp_series_sum_eq_rat [algebra ℚ 𝔸] :
+  (exp_series 𝕂 𝔸).sum = (exp_series ℚ 𝔸).sum :=
+by { ext, simp_rw [exp_series_sum_eq, inv_nat_cast_smul_eq 𝕂 ℚ] }
+
+lemma exp_series_eq_exp_series_rat [algebra ℚ 𝔸] (n : ℕ) (x : 𝔸) :
+  exp_series 𝕂 𝔸 n (λ _, x) = exp_series ℚ 𝔸 n (λ _, x) :=
+by rw [exp_series_apply_eq, exp_series_apply_eq, inv_nat_cast_smul_eq 𝕂 ℚ]
+
+lemma exp_eq_tsum [algebra ℚ 𝔸] : exp = (λ x : 𝔸, ∑' (n : ℕ), (n!⁻¹ : ℚ) • x^n) :=
 funext exp_series_sum_eq
 
-@[simp] lemma exp_zero [t2_space 𝔸] : exp 𝕂 (0 : 𝔸) = 1 :=
+@[simp] lemma exp_zero [algebra ℚ 𝔸] [t2_space 𝔸] : exp (0 : 𝔸) = 1 :=
 begin
-  suffices : (λ x : 𝔸, ∑' (n : ℕ), (n!⁻¹ : 𝕂) • x^n) 0 = ∑' (n : ℕ), if n = 0 then 1 else 0,
+  suffices : (λ x : 𝔸, ∑' (n : ℕ), (n!⁻¹ : ℚ) • x^n) 0 = ∑' (n : ℕ), if n = 0 then 1 else 0,
   { have key : ∀ n ∉ ({0} : finset ℕ), (if n = 0 then (1 : 𝔸) else 0) = 0,
       from λ n hn, if_neg (finset.not_mem_singleton.mp hn),
     rw [exp_eq_tsum, this, tsum_eq_sum key, finset.sum_singleton],
@@ -108,17 +116,20 @@ end
 
 variables (𝕂)
 
-lemma commute.exp_right [t2_space 𝔸] {x y : 𝔸} (h : commute x y) : commute x (exp 𝕂 y) :=
+lemma commute.exp_right [algebra ℚ 𝔸] [t2_space 𝔸] {x y : 𝔸} (h : commute x y) :
+  commute x (exp y) :=
 begin
   rw exp_eq_tsum,
   exact commute.tsum_right x (λ n, (h.pow_right n).smul_right _),
 end
 
-lemma commute.exp_left [t2_space 𝔸] {x y : 𝔸} (h : commute x y) : commute (exp 𝕂 x) y :=
-(h.symm.exp_right 𝕂).symm
+lemma commute.exp_left [algebra ℚ 𝔸] [t2_space 𝔸] {x y : 𝔸} (h : commute x y) :
+  commute (exp x) y :=
+h.symm.exp_right.symm
 
-lemma commute.exp [t2_space 𝔸] {x y : 𝔸} (h : commute x y) : commute (exp 𝕂 x) (exp 𝕂 y) :=
-(h.exp_left _).exp_right _
+lemma commute.exp [algebra ℚ 𝔸] [t2_space 𝔸] {x y : 𝔸} (h : commute x y) :
+  commute (exp x) (exp y) :=
+h.exp_left.exp_right
 
 end topological_algebra
 
@@ -136,7 +147,7 @@ funext (exp_series_apply_eq_div x)
 lemma exp_series_sum_eq_div (x : 𝔸) : (exp_series 𝕂 𝔸).sum x = ∑' (n : ℕ), x^n / n! :=
 tsum_congr (exp_series_apply_eq_div x)
 
-lemma exp_eq_tsum_div : exp 𝕂 = (λ x : 𝔸, ∑' (n : ℕ), x^n / n!) :=
+lemma exp_eq_tsum_div [algebra ℚ 𝔸] : exp = (λ x : 𝔸, ∑' (n : ℕ), x^n / n!) :=
 funext exp_series_sum_eq_div
 
 end topological_division_algebra
@@ -176,33 +187,36 @@ lemma exp_series_summable_of_mem_ball' (x : 𝔸)
   summable (λ n, (n!⁻¹ : 𝕂) • x^n) :=
 summable_of_summable_norm (norm_exp_series_summable_of_mem_ball' x hx)
 
-lemma exp_series_has_sum_exp_of_mem_ball (x : 𝔸)
+lemma exp_series_has_sum_exp_of_mem_ball [algebra ℚ 𝔸] (x : 𝔸)
   (hx : x ∈ emetric.ball (0 : 𝔸) (exp_series 𝕂 𝔸).radius) :
-  has_sum (λ n, exp_series 𝕂 𝔸 n (λ _, x)) (exp 𝕂 x) :=
-formal_multilinear_series.has_sum (exp_series 𝕂 𝔸) hx
+  has_sum (λ n, exp_series 𝕂 𝔸 n (λ _, x)) (exp x) :=
+by simpa only [exp, exp_series_sum_eq_rat] using
+  formal_multilinear_series.has_sum (exp_series 𝕂 𝔸) hx
 
-lemma exp_series_has_sum_exp_of_mem_ball' (x : 𝔸)
+lemma exp_series_has_sum_exp_of_mem_ball' [algebra ℚ 𝔸] (x : 𝔸)
   (hx : x ∈ emetric.ball (0 : 𝔸) (exp_series 𝕂 𝔸).radius) :
-  has_sum (λ n, (n!⁻¹ : 𝕂) • x^n) (exp 𝕂 x):=
+  has_sum (λ n, (n!⁻¹ : 𝕂) • x^n) (exp x) :=
 begin
   rw ← exp_series_apply_eq',
   exact exp_series_has_sum_exp_of_mem_ball x hx
 end
 
-lemma has_fpower_series_on_ball_exp_of_radius_pos (h : 0 < (exp_series 𝕂 𝔸).radius) :
-  has_fpower_series_on_ball (exp 𝕂) (exp_series 𝕂 𝔸) 0 (exp_series 𝕂 𝔸).radius :=
-(exp_series 𝕂 𝔸).has_fpower_series_on_ball h
+lemma has_fpower_series_on_ball_exp_of_radius_pos [algebra ℚ 𝔸] (h : 0 < (exp_series 𝕂 𝔸).radius) :
+  has_fpower_series_on_ball (exp) (exp_series 𝕂 𝔸) 0 (exp_series 𝕂 𝔸).radius :=
+by simpa only [exp, exp_series_sum_eq_rat] using (exp_series 𝕂 𝔸).has_fpower_series_on_ball h
 
-lemma has_fpower_series_at_exp_zero_of_radius_pos (h : 0 < (exp_series 𝕂 𝔸).radius) :
-  has_fpower_series_at (exp 𝕂) (exp_series 𝕂 𝔸) 0 :=
-(has_fpower_series_on_ball_exp_of_radius_pos h).has_fpower_series_at
+lemma has_fpower_series_at_exp_zero_of_radius_pos [algebra ℚ 𝔸] (h : 0 < (exp_series 𝕂 𝔸).radius) :
+  has_fpower_series_at (exp) (exp_series 𝕂 𝔸) 0 :=
+by simpa only [exp, exp_series_sum_eq_rat]
+  using (has_fpower_series_on_ball_exp_of_radius_pos h).has_fpower_series_at
 
-lemma continuous_on_exp :
-  continuous_on (exp 𝕂 : 𝔸 → 𝔸) (emetric.ball 0 (exp_series 𝕂 𝔸).radius) :=
-formal_multilinear_series.continuous_on
+lemma continuous_on_exp [algebra ℚ 𝔸] :
+  continuous_on (exp : 𝔸 → 𝔸) (emetric.ball 0 (exp_series 𝕂 𝔸).radius) :=
+by simpa only [exp, exp_series_sum_eq_rat] using formal_multilinear_series.continuous_on
 
-lemma analytic_at_exp_of_mem_ball (x : 𝔸) (hx : x ∈ emetric.ball (0 : 𝔸) (exp_series 𝕂 𝔸).radius) :
-  analytic_at 𝕂 (exp 𝕂) x:=
+lemma analytic_at_exp_of_mem_ball [algebra ℚ 𝔸] (x : 𝔸)
+  (hx : x ∈ emetric.ball (0 : 𝔸) (exp_series 𝕂 𝔸).radius) :
+  analytic_at 𝕂 (exp) x:=
 begin
   by_cases h : (exp_series 𝕂 𝔸).radius = 0,
   { rw h at hx, exact (ennreal.not_lt_zero hx).elim },
@@ -211,11 +225,11 @@ begin
 end
 
 /-- In a Banach-algebra `𝔸` over a normed field `𝕂` of characteristic zero, if `x` and `y` are
-in the disk of convergence and commute, then `exp 𝕂 (x + y) = (exp 𝕂 x) * (exp 𝕂 y)`. -/
-lemma exp_add_of_commute_of_mem_ball [char_zero 𝕂]
+in the disk of convergence and commute, then `exp (x + y) = (exp x) * (exp y)`. -/
+lemma exp_add_of_commute_of_mem_ball [algebra ℚ 𝔸]
   {x y : 𝔸} (hxy : commute x y) (hx : x ∈ emetric.ball (0 : 𝔸) (exp_series 𝕂 𝔸).radius)
   (hy : y ∈ emetric.ball (0 : 𝔸) (exp_series 𝕂 𝔸).radius) :
-  exp 𝕂 (x + y) = (exp 𝕂 x) * (exp 𝕂 y) :=
+  exp (x + y) = (exp x) * (exp y) :=
 begin
   rw [exp_eq_tsum, tsum_mul_tsum_eq_tsum_sum_antidiagonal_of_summable_norm
         (norm_exp_series_summable_of_mem_ball' x hx) (norm_exp_series_summable_of_mem_ball' y hy)],
@@ -229,10 +243,10 @@ begin
   field_simp [this]
 end
 
-/-- `exp 𝕂 x` has explicit two-sided inverse `exp 𝕂 (-x)`. -/
-noncomputable def invertible_exp_of_mem_ball [char_zero 𝕂] {x : 𝔸}
-  (hx : x ∈ emetric.ball (0 : 𝔸) (exp_series 𝕂 𝔸).radius) : invertible (exp 𝕂 x) :=
-{ inv_of := exp 𝕂 (-x),
+/-- `exp x` has explicit two-sided inverse `exp (-x)`. -/
+noncomputable def invertible_exp_of_mem_ball [algebra ℚ 𝔸] {x : 𝔸}
+  (hx : x ∈ emetric.ball (0 : 𝔸) (exp_series 𝕂 𝔸).radius) : invertible (exp x) :=
+{ inv_of := exp (-x),
   inv_of_mul_self := begin
     have hnx : -x ∈ emetric.ball (0 : 𝔸) (exp_series 𝕂 𝔸).radius,
     { rw [emetric.mem_ball, ←neg_zero, edist_neg_neg],
@@ -248,19 +262,19 @@ noncomputable def invertible_exp_of_mem_ball [char_zero 𝕂] {x : 𝔸}
       exp_zero],
   end }
 
-lemma is_unit_exp_of_mem_ball [char_zero 𝕂] {x : 𝔸}
-  (hx : x ∈ emetric.ball (0 : 𝔸) (exp_series 𝕂 𝔸).radius) : is_unit (exp 𝕂 x) :=
+lemma is_unit_exp_of_mem_ball [algebra ℚ 𝔸] {x : 𝔸}
+  (hx : x ∈ emetric.ball (0 : 𝔸) (exp_series 𝕂 𝔸).radius) : is_unit (exp x) :=
 @is_unit_of_invertible _ _ _ (invertible_exp_of_mem_ball hx)
 
-lemma inv_of_exp_of_mem_ball [char_zero 𝕂] {x : 𝔸}
-  (hx : x ∈ emetric.ball (0 : 𝔸) (exp_series 𝕂 𝔸).radius) [invertible (exp 𝕂 x)] :
-  ⅟(exp 𝕂 x) = exp 𝕂 (-x) :=
-by { letI := invertible_exp_of_mem_ball hx, convert (rfl : ⅟(exp 𝕂 x) = _) }
+lemma inv_of_exp_of_mem_ball [algebra ℚ 𝔸] {x : 𝔸}
+  (hx : x ∈ emetric.ball (0 : 𝔸) (exp_series 𝕂 𝔸).radius) [invertible (exp x)] :
+  ⅟(exp x) = exp (-x) :=
+by { letI := invertible_exp_of_mem_ball hx, convert (rfl : ⅟(exp x) = _) }
 
 /-- Any continuous ring homomorphism commutes with `exp`. -/
-lemma map_exp_of_mem_ball {F} [ring_hom_class F 𝔸 𝔹] (f : F) (hf : continuous f) (x : 𝔸)
+lemma map_exp_of_mem_ball [algebra ℚ 𝔸] [algebra ℚ 𝔹] {F} [ring_hom_class F 𝔸 𝔹] (f : F) (hf : continuous f) (x : 𝔸)
   (hx : x ∈ emetric.ball (0 : 𝔸) (exp_series 𝕂 𝔸).radius) :
-  f (exp 𝕂 x) = exp 𝕂 (f x) :=
+  f (exp x) = exp (f x) :=
 begin
   rw [exp_eq_tsum, exp_eq_tsum],
   refine ((exp_series_summable_of_mem_ball' _ hx).has_sum.map f hf).tsum_eq.symm.trans _,
@@ -270,9 +284,9 @@ end
 
 end complete_algebra
 
-lemma algebra_map_exp_comm_of_mem_ball [complete_space 𝕂] (x : 𝕂)
+lemma algebra_map_exp_comm_of_mem_ball [algebra ℚ 𝔸] [char_zero 𝕂] [complete_space 𝕂] (x : 𝕂)
   (hx : x ∈ emetric.ball (0 : 𝕂) (exp_series 𝕂 𝕂).radius) :
-  algebra_map 𝕂 𝔸 (exp 𝕂 x) = exp 𝕂 (algebra_map 𝕂 𝔸 x) :=
+  algebra_map 𝕂 𝔸 (exp x) = exp (algebra_map 𝕂 𝔸 x) :=
 map_exp_of_mem_ball _ (algebra_map_clm _ _).continuous _ hx
 
 end any_field_any_algebra
@@ -297,7 +311,7 @@ lemma exp_series_div_summable_of_mem_ball [complete_space 𝔸] (x : 𝔸)
 summable_of_summable_norm (norm_exp_series_div_summable_of_mem_ball 𝕂 x hx)
 
 lemma exp_series_div_has_sum_exp_of_mem_ball [complete_space 𝔸] (x : 𝔸)
-  (hx : x ∈ emetric.ball (0 : 𝔸) (exp_series 𝕂 𝔸).radius) : has_sum (λ n, x^n / n!) (exp 𝕂 x) :=
+  (hx : x ∈ emetric.ball (0 : 𝔸) (exp_series 𝕂 𝔸).radius) : has_sum (λ n, x^n / n!) (exp x) :=
 begin
   rw ← exp_series_apply_eq_div' x,
   exact exp_series_has_sum_exp_of_mem_ball x hx
@@ -305,12 +319,12 @@ end
 
 variables {𝕂}
 
-lemma exp_neg_of_mem_ball [char_zero 𝕂] [complete_space 𝔸] {x : 𝔸}
+lemma exp_neg_of_mem_ball [algebra ℚ 𝔸] [complete_space 𝔸] {x : 𝔸}
   (hx : x ∈ emetric.ball (0 : 𝔸) (exp_series 𝕂 𝔸).radius) :
-  exp 𝕂 (-x) = (exp 𝕂 x)⁻¹ :=
+  exp (-x) = (exp x)⁻¹ :=
 begin
   letI := invertible_exp_of_mem_ball hx,
-  exact inv_of_eq_inv (exp 𝕂 x),
+  exact inv_of_eq_inv (exp x),
 end
 
 end any_field_division_algebra
@@ -322,11 +336,11 @@ variables {𝕂 𝔸 : Type*} [nondiscrete_normed_field 𝕂] [normed_comm_ring
   [complete_space 𝔸]
 
 /-- In a commutative Banach-algebra `𝔸` over a normed field `𝕂` of characteristic zero,
-`exp 𝕂 (x+y) = (exp 𝕂 x) * (exp 𝕂 y)` for all `x`, `y` in the disk of convergence. -/
-lemma exp_add_of_mem_ball [char_zero 𝕂] {x y : 𝔸}
+`exp (x+y) = (exp x) * (exp y)` for all `x`, `y` in the disk of convergence. -/
+lemma exp_add_of_mem_ball [algebra ℚ 𝔸] {x y : 𝔸}
   (hx : x ∈ emetric.ball (0 : 𝔸) (exp_series 𝕂 𝔸).radius)
   (hy : y ∈ emetric.ball (0 : 𝔸) (exp_series 𝕂 𝔸).radius) :
-  exp 𝕂 (x + y) = (exp 𝕂 x) * (exp 𝕂 y) :=
+  exp (x + y) = (exp x) * (exp y) :=
 exp_add_of_commute_of_mem_ball (commute.all x y) hx hy
 
 end any_field_comm_algebra
@@ -376,68 +390,75 @@ summable_of_summable_norm (norm_exp_series_summable x)
 lemma exp_series_summable' (x : 𝔸) : summable (λ n, (n!⁻¹ : 𝕂) • x^n) :=
 summable_of_summable_norm (norm_exp_series_summable' x)
 
-lemma exp_series_has_sum_exp (x : 𝔸) : has_sum (λ n, exp_series 𝕂 𝔸 n (λ _, x)) (exp 𝕂 x) :=
+variables [algebra ℚ 𝔸]
+
+lemma exp_series_has_sum_exp (x : 𝔸) :
+  has_sum (λ n, exp_series 𝕂 𝔸 n (λ _, x)) (exp x) :=
 exp_series_has_sum_exp_of_mem_ball x ((exp_series_radius_eq_top 𝕂 𝔸).symm ▸ edist_lt_top _ _)
 
-lemma exp_series_has_sum_exp' (x : 𝔸) : has_sum (λ n, (n!⁻¹ : 𝕂) • x^n) (exp 𝕂 x):=
+lemma exp_series_has_sum_exp' (x : 𝔸) :
+  has_sum (λ n, (n!⁻¹ : 𝕂) • x^n) (exp x):=
 exp_series_has_sum_exp_of_mem_ball' x ((exp_series_radius_eq_top 𝕂 𝔸).symm ▸ edist_lt_top _ _)
 
 lemma exp_has_fpower_series_on_ball :
-  has_fpower_series_on_ball (exp 𝕂) (exp_series 𝕂 𝔸) 0 ∞ :=
+  has_fpower_series_on_ball (exp) (exp_series 𝕂 𝔸) 0 ∞ :=
 exp_series_radius_eq_top 𝕂 𝔸 ▸
   has_fpower_series_on_ball_exp_of_radius_pos (exp_series_radius_pos _ _)
 
 lemma exp_has_fpower_series_at_zero :
-  has_fpower_series_at (exp 𝕂) (exp_series 𝕂 𝔸) 0 :=
+  has_fpower_series_at (exp) (exp_series 𝕂 𝔸) 0 :=
 exp_has_fpower_series_on_ball.has_fpower_series_at
 
-lemma exp_continuous : continuous (exp 𝕂 : 𝔸 → 𝔸) :=
+section
+include 𝕂
+lemma exp_continuous : continuous (exp : 𝔸 → 𝔸) :=
 begin
   rw [continuous_iff_continuous_on_univ, ← metric.eball_top_eq_univ (0 : 𝔸),
       ← exp_series_radius_eq_top 𝕂 𝔸],
   exact continuous_on_exp
 end
+end
 
 lemma exp_analytic (x : 𝔸) :
-  analytic_at 𝕂 (exp 𝕂) x :=
+  analytic_at 𝕂 (exp) x :=
 analytic_at_exp_of_mem_ball x ((exp_series_radius_eq_top 𝕂 𝔸).symm ▸ edist_lt_top _ _)
 
 /-- In a Banach-algebra `𝔸` over `𝕂 = ℝ` or `𝕂 = ℂ`, if `x` and `y` commute, then
-`exp 𝕂 (x+y) = (exp 𝕂 x) * (exp 𝕂 y)`. -/
+`exp (x+y) = (exp x) * (exp y)`. -/
 lemma exp_add_of_commute
   {x y : 𝔸} (hxy : commute x y) :
-  exp 𝕂 (x + y) = (exp 𝕂 x) * (exp 𝕂 y) :=
+  exp (x + y) = (exp x) * (exp y) :=
 exp_add_of_commute_of_mem_ball hxy ((exp_series_radius_eq_top 𝕂 𝔸).symm ▸ edist_lt_top _ _)
   ((exp_series_radius_eq_top 𝕂 𝔸).symm ▸ edist_lt_top _ _)
 
 section
 variables (𝕂)
 
-/-- `exp 𝕂 x` has explicit two-sided inverse `exp 𝕂 (-x)`. -/
-noncomputable def invertible_exp (x : 𝔸) : invertible (exp 𝕂 x) :=
+/-- `exp x` has explicit two-sided inverse `exp (-x)`. -/
+noncomputable def invertible_exp (x : 𝔸) : invertible (exp x) :=
 invertible_exp_of_mem_ball $ (exp_series_radius_eq_top 𝕂 𝔸).symm ▸ edist_lt_top _ _
 
-lemma is_unit_exp (x : 𝔸) : is_unit (exp 𝕂 x) :=
+lemma is_unit_exp (x : 𝔸) : is_unit (exp x) :=
 is_unit_exp_of_mem_ball $ (exp_series_radius_eq_top 𝕂 𝔸).symm ▸ edist_lt_top _ _
 
-lemma inv_of_exp (x : 𝔸) [invertible (exp 𝕂 x)] :
-  ⅟(exp 𝕂 x) = exp 𝕂 (-x) :=
+lemma inv_of_exp (x : 𝔸) [invertible (exp x)] :
+  ⅟(exp x) = exp (-x) :=
 inv_of_exp_of_mem_ball $ (exp_series_radius_eq_top 𝕂 𝔸).symm ▸ edist_lt_top _ _
 
-lemma ring.inverse_exp (x : 𝔸) : ring.inverse (exp 𝕂 x) = exp 𝕂 (-x) :=
+lemma ring.inverse_exp (x : 𝔸) : ring.inverse (exp x) = exp (-x) :=
 begin
-  letI := invertible_exp 𝕂 x,
+  letI := invertible_exp x,
   exact ring.inverse_invertible _,
 end
 
 end
 
 /-- In a Banach-algebra `𝔸` over `𝕂 = ℝ` or `𝕂 = ℂ`, if a family of elements `f i` mutually
-commute then `exp 𝕂 (∑ i, f i) = ∏ i, exp 𝕂 (f i)`. -/
+commute then `exp (∑ i, f i) = ∏ i, exp (f i)`. -/
 lemma exp_sum_of_commute {ι} (s : finset ι) (f : ι → 𝔸)
   (h : ∀ (i ∈ s) (j ∈ s), commute (f i) (f j)) :
-  exp 𝕂 (∑ i in s, f i) = s.noncomm_prod (λ i, exp 𝕂 (f i))
-    (λ i hi j hj, (h i hi j hj).exp 𝕂) :=
+  exp (∑ i in s, f i) = s.noncomm_prod (λ i, exp (f i))
+    (λ i hi j hj, (h i hi j hj).exp) :=
 begin
   classical,
   induction s using finset.induction_on with a s ha ih,
@@ -450,7 +471,7 @@ begin
 end
 
 lemma exp_nsmul (n : ℕ) (x : 𝔸) :
-  exp 𝕂 (n • x) = exp 𝕂 x ^ n :=
+  exp (n • x) = exp x ^ n :=
 begin
   induction n with n ih,
   { rw [zero_smul, pow_zero, exp_zero], },
@@ -461,32 +482,32 @@ variables (𝕂)
 
 /-- Any continuous ring homomorphism commutes with `exp`. -/
 lemma map_exp {F} [ring_hom_class F 𝔸 𝔹] (f : F) (hf : continuous f) (x : 𝔸) :
-  f (exp 𝕂 x) = exp 𝕂 (f x) :=
+  f (exp x) = exp (f x) :=
 map_exp_of_mem_ball f hf x $ (exp_series_radius_eq_top 𝕂 𝔸).symm ▸ edist_lt_top _ _
 
 lemma exp_smul {G} [monoid G] [mul_semiring_action G 𝔸] [has_continuous_const_smul G 𝔸]
   (g : G) (x : 𝔸) :
-  exp 𝕂 (g • x) = g • exp 𝕂 x :=
-(map_exp 𝕂 (mul_semiring_action.to_ring_hom G 𝔸 g) (continuous_const_smul _) x).symm
+  exp (g • x) = g • exp x :=
+(map_exp (mul_semiring_action.to_ring_hom G 𝔸 g) (continuous_const_smul _) x).symm
 
 lemma exp_units_conj (y : 𝔸ˣ) (x : 𝔸)  :
-  exp 𝕂 (y * x * ↑(y⁻¹) : 𝔸) = y * exp 𝕂 x * ↑(y⁻¹) :=
+  exp (y * x * ↑(y⁻¹) : 𝔸) = y * exp x * ↑(y⁻¹) :=
 exp_smul _ (conj_act.to_conj_act y) x
 
 lemma exp_units_conj' (y : 𝔸ˣ) (x : 𝔸)  :
-  exp 𝕂 (↑(y⁻¹) * x * y) = ↑(y⁻¹) * exp 𝕂 x * y :=
+  exp (↑(y⁻¹) * x * y) = ↑(y⁻¹) * exp x * y :=
 exp_units_conj _ _ _
 
-@[simp] lemma prod.fst_exp [complete_space 𝔹] (x : 𝔸 × 𝔹) : (exp 𝕂 x).fst = exp 𝕂 x.fst :=
+@[simp] lemma prod.fst_exp [complete_space 𝔹] (x : 𝔸 × 𝔹) : (exp x).fst = exp x.fst :=
 map_exp _ (ring_hom.fst 𝔸 𝔹) continuous_fst x
 
-@[simp] lemma prod.snd_exp [complete_space 𝔹] (x : 𝔸 × 𝔹) : (exp 𝕂 x).snd = exp 𝕂 x.snd :=
+@[simp] lemma prod.snd_exp [complete_space 𝔹] (x : 𝔸 × 𝔹) : (exp x).snd = exp x.snd :=
 map_exp _ (ring_hom.snd 𝔸 𝔹) continuous_snd x
 
 @[simp] lemma pi.exp_apply {ι : Type*} {𝔸 : ι → Type*} [fintype ι]
   [Π i, normed_ring (𝔸 i)] [Π i, normed_algebra 𝕂 (𝔸 i)] [Π i, complete_space (𝔸 i)]
   (x : Π i, 𝔸 i) (i : ι) :
-  exp 𝕂 x i = exp 𝕂 (x i) :=
+  exp x i = exp (x i) :=
 begin
   -- Lean struggles to infer this instance due to it wanting `[Π i, semi_normed_ring (𝔸 i)]`
   letI : normed_algebra 𝕂 (Π i, 𝔸 i) := pi.normed_algebra _,
@@ -496,23 +517,23 @@ end
 lemma pi.exp_def {ι : Type*} {𝔸 : ι → Type*} [fintype ι]
   [Π i, normed_ring (𝔸 i)] [Π i, normed_algebra 𝕂 (𝔸 i)] [Π i, complete_space (𝔸 i)]
   (x : Π i, 𝔸 i) :
-  exp 𝕂 x = λ i, exp 𝕂 (x i) :=
+  exp x = λ i, exp (x i) :=
 funext $ pi.exp_apply 𝕂 x
 
 lemma function.update_exp {ι : Type*} {𝔸 : ι → Type*} [fintype ι] [decidable_eq ι]
   [Π i, normed_ring (𝔸 i)] [Π i, normed_algebra 𝕂 (𝔸 i)] [Π i, complete_space (𝔸 i)]
   (x : Π i, 𝔸 i) (j : ι) (xj : 𝔸 j) :
-  function.update (exp 𝕂 x) j (exp 𝕂 xj) = exp 𝕂 (function.update x j xj) :=
+  function.update (exp x) j (exp xj) = exp (function.update x j xj) :=
 begin
   ext i,
   simp_rw [pi.exp_def],
-  exact (function.apply_update (λ i, exp 𝕂) x j xj i).symm,
+  exact (function.apply_update (λ i, exp) x j xj i).symm,
 end
 
 end complete_algebra
 
 lemma algebra_map_exp_comm (x : 𝕂) :
-  algebra_map 𝕂 𝔸 (exp 𝕂 x) = exp 𝕂 (algebra_map 𝕂 𝔸 x) :=
+  algebra_map 𝕂 𝔸 (exp x) = exp (algebra_map 𝕂 𝔸 x) :=
 algebra_map_exp_comm_of_mem_ball x $
   (exp_series_radius_eq_top 𝕂 𝕂).symm ▸ edist_lt_top _ _
 
@@ -533,16 +554,16 @@ variables [complete_space 𝔸]
 lemma exp_series_div_summable (x : 𝔸) : summable (λ n, x^n / n!) :=
 summable_of_summable_norm (norm_exp_series_div_summable 𝕂 x)
 
-lemma exp_series_div_has_sum_exp (x : 𝔸) : has_sum (λ n, x^n / n!) (exp 𝕂 x):=
+lemma exp_series_div_has_sum_exp (x : 𝔸) : has_sum (λ n, x^n / n!) (exp x):=
 exp_series_div_has_sum_exp_of_mem_ball 𝕂 x
   ((exp_series_radius_eq_top 𝕂 𝔸).symm ▸ edist_lt_top _ _)
 
-variables {𝕂}
+variables {𝕂} [algebra ℚ 𝔸]
 
-lemma exp_neg (x : 𝔸) : exp 𝕂 (-x) = (exp 𝕂 x)⁻¹ :=
+lemma exp_neg (x : 𝔸) : exp (-x) = (exp x)⁻¹ :=
 exp_neg_of_mem_ball $ (exp_series_radius_eq_top 𝕂 𝔸).symm ▸ edist_lt_top _ _
 
-lemma exp_zsmul (z : ℤ) (x : 𝔸) : exp 𝕂 (z • x) = (exp 𝕂 x) ^ z :=
+lemma exp_zsmul (z : ℤ) (x : 𝔸) : exp (z • x) = (exp x) ^ z :=
 begin
   obtain ⟨n, rfl | rfl⟩ := z.eq_coe_or_neg,
   { rw [zpow_coe_nat, coe_nat_zsmul, exp_nsmul] },
@@ -550,11 +571,11 @@ begin
 end
 
 lemma exp_conj (y : 𝔸) (x : 𝔸) (hy : y ≠ 0) :
-  exp 𝕂 (y * x * y⁻¹) = y * exp 𝕂 x * y⁻¹ :=
+  exp (y * x * y⁻¹) = y * exp x * y⁻¹ :=
 exp_units_conj _ (units.mk0 y hy) x
 
 lemma exp_conj' (y : 𝔸) (x : 𝔸)  (hy : y ≠ 0) :
-  exp 𝕂 (y⁻¹ * x * y) = y⁻¹ * exp 𝕂 x * y :=
+  exp (y⁻¹ * x * y) = y⁻¹ * exp x * y :=
 exp_units_conj' _ (units.mk0 y hy) x
 
 end division_algebra
@@ -563,15 +584,17 @@ section comm_algebra
 
 variables {𝕂 𝔸 : Type*} [is_R_or_C 𝕂] [normed_comm_ring 𝔸] [normed_algebra 𝕂 𝔸] [complete_space 𝔸]
 
+variables  [algebra ℚ 𝔸]
+
 /-- In a commutative Banach-algebra `𝔸` over `𝕂 = ℝ` or `𝕂 = ℂ`,
-`exp 𝕂 (x+y) = (exp 𝕂 x) * (exp 𝕂 y)`. -/
-lemma exp_add {x y : 𝔸} : exp 𝕂 (x + y) = (exp 𝕂 x) * (exp 𝕂 y) :=
+`exp (x+y) = (exp x) * (exp y)`. -/
+lemma exp_add {x y : 𝔸} : exp (x + y) = (exp x) * (exp y) :=
 exp_add_of_mem_ball ((exp_series_radius_eq_top 𝕂 𝔸).symm ▸ edist_lt_top _ _)
   ((exp_series_radius_eq_top 𝕂 𝔸).symm ▸ edist_lt_top _ _)
 
 /-- A version of `exp_sum_of_commute` for a commutative Banach-algebra. -/
 lemma exp_sum {ι} (s : finset ι) (f : ι → 𝔸) :
-  exp 𝕂 (∑ i in s, f i) = ∏ i in s, exp 𝕂 (f i) :=
+  exp (∑ i in s, f i) = ∏ i in s, exp (f i) :=
 begin
   rw [exp_sum_of_commute, finset.noncomm_prod_eq_prod],
   exact λ i hi j hj, commute.all _ _,
@@ -594,24 +617,11 @@ lemma exp_series_eq_exp_series (n : ℕ) (x : 𝔸) :
   (exp_series 𝕂 𝔸 n (λ _, x)) = (exp_series 𝕂' 𝔸 n (λ _, x)) :=
 by rw [exp_series_apply_eq, exp_series_apply_eq, inv_nat_cast_smul_eq 𝕂 𝕂']
 
-/-- If a normed ring `𝔸` is a normed algebra over two fields, then they define the same
-exponential function on `𝔸`. -/
-lemma exp_eq_exp : (exp 𝕂 : 𝔸 → 𝔸) = exp 𝕂' :=
-begin
-  ext,
-  rw [exp, exp],
-  refine tsum_congr (λ n, _),
-  rw exp_series_eq_exp_series 𝕂 𝕂' 𝔸 n x
-end
-
-lemma exp_ℝ_ℂ_eq_exp_ℂ_ℂ : (exp ℝ : ℂ → ℂ) = exp ℂ :=
-exp_eq_exp ℝ ℂ ℂ
-
 end scalar_tower
 
 lemma star_exp {𝕜 A : Type*} [is_R_or_C 𝕜] [normed_ring A] [normed_algebra 𝕜 A]
-  [star_ring A] [normed_star_group A] [complete_space A]
-  [star_module 𝕜 A] (a : A) : star (exp 𝕜 a) = exp 𝕜 (star a) :=
+  [star_ring A] [normed_star_group A] [complete_space A]  [algebra ℚ A]
+  [star_module 𝕜 A] (a : A) : star (exp a) = exp (star a) :=
 begin
   rw exp_eq_tsum,
   have := continuous_linear_map.map_tsum

From b6a69bf4a6e69f4cc0f87087f9568513f344270e Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Sun, 12 Nov 2023 12:55:41 +0000
Subject: [PATCH 6/6] fix

---
 src/analysis/normed_space/exponential.lean    | 14 ++--
 .../normed_space/matrix_exponential.lean      | 80 +++++++++++--------
 2 files changed, 53 insertions(+), 41 deletions(-)

diff --git a/src/analysis/normed_space/exponential.lean b/src/analysis/normed_space/exponential.lean
index 350ad883d21e0..54f8921dca8b4 100644
--- a/src/analysis/normed_space/exponential.lean
+++ b/src/analysis/normed_space/exponential.lean
@@ -181,7 +181,7 @@ section normed
 section any_field_any_algebra
 
 variables {𝕂 𝔸 𝔹 : Type*} [nontrivially_normed_field 𝕂]
-variables [normed_ring 𝔸] [normed_ring 𝔹] [normed_algebra 𝕂 𝔸] [normed_algebra 𝕂 𝔹]
+variables [normed_ring 𝔸] [normed_ring 𝔹] [normed_algebra 𝕂 𝔸]
 
 lemma norm_exp_series_summable_of_mem_ball (x : 𝔸)
   (hx : x ∈ emetric.ball (0 : 𝔸) (exp_series 𝕂 𝔸).radius) :
@@ -381,7 +381,7 @@ section is_R_or_C
 section any_algebra
 
 variables (𝕂 𝔸 𝔹 : Type*) [is_R_or_C 𝕂] [normed_ring 𝔸] [normed_algebra 𝕂 𝔸]
-variables [normed_ring 𝔹] [normed_algebra 𝕂 𝔹]
+variables [normed_ring 𝔹]
 
 /-- In a normed algebra `𝔸` over `𝕂 = ℝ` or `𝕂 = ℂ`, the series defining the exponential map
 has an infinite radius of convergence. -/
@@ -549,10 +549,10 @@ lemma exp_units_conj' (y : 𝔸ˣ) (x : 𝔸)  :
   exp (↑(y⁻¹) * x * y) = ↑(y⁻¹) * exp x * y :=
 exp_units_conj 𝕂 _ _
 
-@[simp] lemma prod.fst_exp [complete_space 𝔹] (x : 𝔸 × 𝔹) : (exp x).fst = exp x.fst :=
+@[simp] lemma prod.fst_exp [normed_algebra 𝕂 𝔹] [complete_space 𝔹] (x : 𝔸 × 𝔹) : (exp x).fst = exp x.fst :=
 map_exp 𝕂 (ring_hom.fst 𝔸 𝔹) continuous_fst x
 
-@[simp] lemma prod.snd_exp [complete_space 𝔹] (x : 𝔸 × 𝔹) : (exp x).snd = exp x.snd :=
+@[simp] lemma prod.snd_exp [normed_algebra 𝕂 𝔹] [complete_space 𝔹] (x : 𝔸 × 𝔹) : (exp x).snd = exp x.snd :=
 map_exp 𝕂 (ring_hom.snd 𝔸 𝔹) continuous_snd x
 
 @[simp] lemma pi.exp_apply {ι : Type*} {𝔸 : ι → Type*} [fintype ι]
@@ -605,16 +605,18 @@ lemma norm_exp_series_div_summable (x : 𝔸) : summable (λ n, ‖x^n / n!‖)
 norm_exp_series_div_summable_of_mem_ball 𝕂 x
   ((exp_series_radius_eq_top 𝕂 𝔸).symm ▸ edist_lt_top _ _)
 
-variables [complete_space 𝔸] [algebra ℚ 𝔸]
+variables [complete_space 𝔸]
 
 lemma exp_series_div_summable (x : 𝔸) : summable (λ n, x^n / n!) :=
 summable_of_summable_norm (norm_exp_series_div_summable 𝕂 x)
 
+variables [algebra ℚ 𝔸]
+
 lemma exp_series_div_has_sum_exp (x : 𝔸) : has_sum (λ n, x^n / n!) (exp x):=
 exp_series_div_has_sum_exp_of_mem_ball 𝕂 x
   ((exp_series_radius_eq_top 𝕂 𝔸).symm ▸ edist_lt_top _ _)
 
-variables (𝕂) [algebra ℚ 𝔸]
+variables (𝕂)
 
 lemma exp_neg (x : 𝔸) : exp (-x) = (exp x)⁻¹ :=
 exp_neg_of_mem_ball 𝕂 $ (exp_series_radius_eq_top 𝕂 𝔸).symm ▸ edist_lt_top _ _
diff --git a/src/analysis/normed_space/matrix_exponential.lean b/src/analysis/normed_space/matrix_exponential.lean
index 678d4710a310b..ef0bed63797fb 100644
--- a/src/analysis/normed_space/matrix_exponential.lean
+++ b/src/analysis/normed_space/matrix_exponential.lean
@@ -60,7 +60,7 @@ Hopefully we will be able to remove these in Lean 4.
 
 ## TODO
 
-* Show that `matrix.det (exp 𝕂 A) = exp 𝕂 (matrix.trace A)`
+* Show that `matrix.det (exp A) = exp (matrix.trace A)`
 
 ## References
 
@@ -106,38 +106,39 @@ section topological
 section ring
 variables [fintype m] [decidable_eq m] [fintype n] [decidable_eq n]
   [Π i, fintype (n' i)] [Π i, decidable_eq (n' i)]
-  [field 𝕂] [ring 𝔸] [topological_space 𝔸] [topological_ring 𝔸] [algebra 𝕂 𝔸] [t2_space 𝔸]
+  [field 𝕂] [ring 𝔸] [topological_space 𝔸] [topological_ring 𝔸] [algebra 𝕂 𝔸] [algebra ℚ 𝔸]
+  [t2_space 𝔸]
 
-lemma exp_diagonal (v : m → 𝔸) : exp 𝕂 (diagonal v) = diagonal (exp 𝕂 v) :=
+lemma exp_diagonal (v : m → 𝔸) : exp (diagonal v) = diagonal (exp v) :=
 by simp_rw [exp_eq_tsum, diagonal_pow, ←diagonal_smul, ←diagonal_tsum]
 
 lemma exp_block_diagonal (v : m → matrix n n 𝔸) :
-  exp 𝕂 (block_diagonal v) = block_diagonal (exp 𝕂 v) :=
+  exp (block_diagonal v) = block_diagonal (exp v) :=
 by simp_rw [exp_eq_tsum, ←block_diagonal_pow, ←block_diagonal_smul, ←block_diagonal_tsum]
 
 lemma exp_block_diagonal' (v : Π i, matrix (n' i) (n' i) 𝔸) :
-  exp 𝕂 (block_diagonal' v) = block_diagonal' (exp 𝕂 v) :=
+  exp (block_diagonal' v) = block_diagonal' (exp v) :=
 by simp_rw [exp_eq_tsum, ←block_diagonal'_pow, ←block_diagonal'_smul, ←block_diagonal'_tsum]
 
 lemma exp_conj_transpose [star_ring 𝔸] [has_continuous_star 𝔸] (A : matrix m m 𝔸) :
-  exp 𝕂 Aᴴ = (exp 𝕂 A)ᴴ :=
+  exp Aᴴ = (exp A)ᴴ :=
 (star_exp A).symm
 
 lemma is_hermitian.exp [star_ring 𝔸] [has_continuous_star 𝔸] {A : matrix m m 𝔸}
-  (h : A.is_hermitian) : (exp 𝕂 A).is_hermitian :=
-(exp_conj_transpose _ _).symm.trans $ congr_arg _ h
+  (h : A.is_hermitian) : (exp A).is_hermitian :=
+(exp_conj_transpose _).symm.trans $ congr_arg _ h
 
 end ring
 
 section comm_ring
 variables [fintype m] [decidable_eq m] [field 𝕂]
-  [comm_ring 𝔸] [topological_space 𝔸] [topological_ring 𝔸] [algebra 𝕂 𝔸] [t2_space 𝔸]
+  [comm_ring 𝔸] [topological_space 𝔸] [topological_ring 𝔸] [algebra 𝕂 𝔸] [algebra ℚ 𝔸] [t2_space 𝔸]
 
-lemma exp_transpose (A : matrix m m 𝔸) : exp 𝕂 Aᵀ = (exp 𝕂 A)ᵀ :=
+lemma exp_transpose (A : matrix m m 𝔸) : exp Aᵀ = (exp A)ᵀ :=
 by simp_rw [exp_eq_tsum, transpose_tsum, transpose_smul, transpose_pow]
 
-lemma is_symm.exp {A : matrix m m 𝔸} (h : A.is_symm) : (exp 𝕂 A).is_symm :=
-(exp_transpose _ _).symm.trans $ congr_arg _ h
+lemma is_symm.exp {A : matrix m m 𝔸} (h : A.is_symm) : (exp A).is_symm :=
+(exp_transpose _).symm.trans $ congr_arg _ h
 
 end comm_ring
 
@@ -149,56 +150,61 @@ variables [is_R_or_C 𝕂]
   [fintype m] [decidable_eq m]
   [fintype n] [decidable_eq n]
   [Π i, fintype (n' i)] [Π i, decidable_eq (n' i)]
-  [normed_ring 𝔸] [normed_algebra 𝕂 𝔸] [complete_space 𝔸]
+  [normed_ring 𝔸] [algebra ℚ 𝔸] [normed_algebra 𝕂 𝔸] [complete_space 𝔸]
 
 lemma exp_add_of_commute (A B : matrix m m 𝔸) (h : commute A B) :
-  exp 𝕂 (A + B) = exp 𝕂 A ⬝ exp 𝕂 B :=
+  exp (A + B) = exp A ⬝ exp B :=
+let 𝕂 := 𝕂 in
 begin
   letI : semi_normed_ring (matrix m m 𝔸) := matrix.linfty_op_semi_normed_ring,
   letI : normed_ring (matrix m m 𝔸) := matrix.linfty_op_normed_ring,
   letI : normed_algebra 𝕂 (matrix m m 𝔸) := matrix.linfty_op_normed_algebra,
-  exact exp_add_of_commute h,
+  exact exp_add_of_commute 𝕂 h,
 end
 
 lemma exp_sum_of_commute {ι} (s : finset ι) (f : ι → matrix m m 𝔸)
   (h : (s : set ι).pairwise $ λ i j, commute (f i) (f j)) :
-  exp 𝕂 (∑ i in s, f i) = s.noncomm_prod (λ i, exp 𝕂 (f i))
-    (λ i hi j hj _, (h.of_refl hi hj).exp 𝕂) :=
+  exp (∑ i in s, f i) = s.noncomm_prod (λ i, exp (f i))
+    (λ i hi j hj _, (h.of_refl hi hj).exp) :=
+let 𝕂 := 𝕂 in
 begin
   letI : semi_normed_ring (matrix m m 𝔸) := matrix.linfty_op_semi_normed_ring,
   letI : normed_ring (matrix m m 𝔸) := matrix.linfty_op_normed_ring,
   letI : normed_algebra 𝕂 (matrix m m 𝔸) := matrix.linfty_op_normed_algebra,
-  exact exp_sum_of_commute s f h,
+  exact exp_sum_of_commute 𝕂 s f h,
 end
 
 lemma exp_nsmul (n : ℕ) (A : matrix m m 𝔸) :
-  exp 𝕂 (n • A) = exp 𝕂 A ^ n :=
+  exp (n • A) = exp A ^ n :=
+let 𝕂 := 𝕂 in
 begin
   letI : semi_normed_ring (matrix m m 𝔸) := matrix.linfty_op_semi_normed_ring,
   letI : normed_ring (matrix m m 𝔸) := matrix.linfty_op_normed_ring,
   letI : normed_algebra 𝕂 (matrix m m 𝔸) := matrix.linfty_op_normed_algebra,
-  exact exp_nsmul n A,
+  exact exp_nsmul 𝕂 n A,
 end
 
-lemma is_unit_exp (A : matrix m m 𝔸) : is_unit (exp 𝕂 A) :=
+lemma is_unit_exp (A : matrix m m 𝔸) : is_unit (exp A) :=
+let 𝕂 := 𝕂 in
 begin
   letI : semi_normed_ring (matrix m m 𝔸) := matrix.linfty_op_semi_normed_ring,
   letI : normed_ring (matrix m m 𝔸) := matrix.linfty_op_normed_ring,
   letI : normed_algebra 𝕂 (matrix m m 𝔸) := matrix.linfty_op_normed_algebra,
-  exact is_unit_exp _ A,
+  exact is_unit_exp 𝕂 A,
 end
 
 lemma exp_units_conj (U : (matrix m m 𝔸)ˣ) (A : matrix m m 𝔸)  :
-  exp 𝕂 (↑U ⬝ A ⬝ ↑(U⁻¹) : matrix m m 𝔸) = ↑U ⬝ exp 𝕂 A ⬝ ↑(U⁻¹) :=
+  exp (↑U ⬝ A ⬝ ↑(U⁻¹) : matrix m m 𝔸) = ↑U ⬝ exp A ⬝ ↑(U⁻¹) :=
+let 𝕂 := 𝕂 in
 begin
   letI : semi_normed_ring (matrix m m 𝔸) := matrix.linfty_op_semi_normed_ring,
   letI : normed_ring (matrix m m 𝔸) := matrix.linfty_op_normed_ring,
   letI : normed_algebra 𝕂 (matrix m m 𝔸) := matrix.linfty_op_normed_algebra,
-  exact exp_units_conj _ U A,
+  exact exp_units_conj 𝕂 U A,
 end
 
 lemma exp_units_conj' (U : (matrix m m 𝔸)ˣ) (A : matrix m m 𝔸)  :
-  exp 𝕂 (↑(U⁻¹) ⬝ A ⬝ U : matrix m m 𝔸) = ↑(U⁻¹) ⬝ exp 𝕂 A ⬝ U :=
+  exp (↑(U⁻¹) ⬝ A ⬝ U : matrix m m 𝔸) = ↑(U⁻¹) ⬝ exp A ⬝ U :=
 exp_units_conj 𝕂 U⁻¹ A
 
 end normed
@@ -209,32 +215,36 @@ variables [is_R_or_C 𝕂]
   [fintype m] [decidable_eq m]
   [fintype n] [decidable_eq n]
   [Π i, fintype (n' i)] [Π i, decidable_eq (n' i)]
-  [normed_comm_ring 𝔸] [normed_algebra 𝕂 𝔸] [complete_space 𝔸]
+  [normed_comm_ring 𝔸] [algebra ℚ 𝔸] [normed_algebra 𝕂 𝔸] [complete_space 𝔸]
 
-lemma exp_neg (A : matrix m m 𝔸) : exp 𝕂 (-A) = (exp 𝕂 A)⁻¹ :=
+lemma exp_neg (A : matrix m m 𝔸) : exp (-A) = (exp A)⁻¹ :=
+let 𝕂 := 𝕂 in
 begin
   rw nonsing_inv_eq_ring_inverse,
   letI : semi_normed_ring (matrix m m 𝔸) := matrix.linfty_op_semi_normed_ring,
   letI : normed_ring (matrix m m 𝔸) := matrix.linfty_op_normed_ring,
   letI : normed_algebra 𝕂 (matrix m m 𝔸) := matrix.linfty_op_normed_algebra,
-  exact (ring.inverse_exp _ A).symm,
+  exact (ring.inverse_exp 𝕂 A).symm,
 end
 
-lemma exp_zsmul (z : ℤ) (A : matrix m m 𝔸) : exp 𝕂 (z • A) = exp 𝕂 A ^ z :=
+lemma exp_zsmul (z : ℤ) (A : matrix m m 𝔸) : exp (z • A) = exp A ^ z :=
+let 𝕂 := 𝕂 in
 begin
   obtain ⟨n, rfl | rfl⟩ := z.eq_coe_or_neg,
-  { rw [zpow_coe_nat, coe_nat_zsmul, exp_nsmul] },
-  { have : is_unit (exp 𝕂 A).det := (matrix.is_unit_iff_is_unit_det _).mp (is_unit_exp _ _),
-    rw [matrix.zpow_neg this, zpow_coe_nat, neg_smul,
-        exp_neg, coe_nat_zsmul, exp_nsmul] },
+  { rw [zpow_coe_nat, coe_nat_zsmul, exp_nsmul 𝕂]; apply_instance },
+  { have : is_unit (exp A).det := (matrix.is_unit_iff_is_unit_det _).mp (is_unit_exp 𝕂 _),
+    rw [matrix.zpow_neg this, zpow_coe_nat, neg_smul, exp_neg 𝕂, coe_nat_zsmul, exp_nsmul 𝕂];
+      apply_instance },
 end
 
 lemma exp_conj (U : matrix m m 𝔸) (A : matrix m m 𝔸) (hy : is_unit U) :
-  exp 𝕂 (U ⬝ A ⬝ U⁻¹) = U ⬝ exp 𝕂 A ⬝ U⁻¹ :=
+  exp (U ⬝ A ⬝ U⁻¹) = U ⬝ exp A ⬝ U⁻¹ :=
+let 𝕂 := 𝕂 in
 let ⟨u, hu⟩ := hy in hu ▸ by simpa only [matrix.coe_units_inv] using exp_units_conj 𝕂 u A
 
 lemma exp_conj' (U : matrix m m 𝔸) (A : matrix m m 𝔸) (hy : is_unit U) :
-  exp 𝕂 (U⁻¹ ⬝ A ⬝ U) = U⁻¹ ⬝ exp 𝕂 A ⬝ U :=
+  exp (U⁻¹ ⬝ A ⬝ U) = U⁻¹ ⬝ exp A ⬝ U :=
+let 𝕂 := 𝕂 in
 let ⟨u, hu⟩ := hy in hu ▸ by simpa only [matrix.coe_units_inv] using exp_units_conj' 𝕂 u A
 
 end normed_comm