chore: exp -> NormedSpace.exp (#8436)

kim-em · kim-em · commit e4e3f2f5db76 · 2023-11-17T14:37:26.000Z
Per discussion at [zulip](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Real.2Eexp/near/401485920) Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
diff --git a/Mathlib/Analysis/NormedSpace/DualNumber.lean b/Mathlib/Analysis/NormedSpace/DualNumber.lean
@@ -19,6 +19,7 @@ These are just restatements of similar statements about `TrivSqZeroExt R M`.
 
 -/
 
+open NormedSpace -- For `exp`.
 
 namespace DualNumber
 
diff --git a/Mathlib/Analysis/NormedSpace/Exponential.lean b/Mathlib/Analysis/NormedSpace/Exponential.lean
diff --git a/Mathlib/Analysis/NormedSpace/MatrixExponential.lean b/Mathlib/Analysis/NormedSpace/MatrixExponential.lean
@@ -62,6 +62,8 @@ results for general rings are instead stated about `Ring.inverse`:
 
 open scoped Matrix BigOperators
 
+open NormedSpace -- For `exp`.
+
 variable (𝕂 : Type*) {m n p : Type*} {n' : m → Type*} {𝔸 : Type*}
 
 namespace Matrix
diff --git a/Mathlib/Analysis/NormedSpace/QuaternionExponential.lean b/Mathlib/Analysis/NormedSpace/QuaternionExponential.lean
@@ -24,9 +24,10 @@ This file contains results about `exp` on `Quaternion ℝ`.
 
 -/
 
-
 open scoped Quaternion Nat
 
+open NormedSpace
+
 namespace Quaternion
 
 @[simp, norm_cast]
diff --git a/Mathlib/Analysis/NormedSpace/Spectrum.lean b/Mathlib/Analysis/NormedSpace/Spectrum.lean
@@ -47,6 +47,8 @@ This file contains the basic theory for the resolvent and spectrum of a Banach a
 
 open scoped ENNReal NNReal
 
+open NormedSpace -- For `exp`.
+
 /-- The *spectral radius* is the supremum of the `nnnorm` (`‖·‖₊`) of elements in the spectrum,
     coerced into an element of `ℝ≥0∞`. Note that it is possible for `spectrum 𝕜 a = ∅`. In this
     case, `spectralRadius a = 0`. It is also possible that `spectrum 𝕜 a` be unbounded (though
diff --git a/Mathlib/Analysis/NormedSpace/Star/Exponential.lean b/Mathlib/Analysis/NormedSpace/Star/Exponential.lean
@@ -20,6 +20,7 @@ subtypes `selfAdjoint A` and `unitary A`.
   unitaries.
 -/
 
+open NormedSpace -- For `exp`.
 
 section Star
 
diff --git a/Mathlib/Analysis/NormedSpace/Star/Spectrum.lean b/Mathlib/Analysis/NormedSpace/Star/Spectrum.lean
@@ -21,7 +21,7 @@ section
 
 open scoped Topology ENNReal
 
-open Filter ENNReal spectrum CstarRing
+open Filter ENNReal spectrum CstarRing NormedSpace
 
 section UnitarySpectrum
 
@@ -91,7 +91,7 @@ theorem IsSelfAdjoint.mem_spectrum_eq_re [StarModule ℂ A] {a : A} (ha : IsSelf
     (hz : z ∈ spectrum ℂ a) : z = z.re := by
   have hu := exp_mem_unitary_of_mem_skewAdjoint ℂ (ha.smul_mem_skewAdjoint conj_I)
   let Iu := Units.mk0 I I_ne_zero
-  have : _root_.exp ℂ (I • z) ∈ spectrum ℂ (_root_.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
diff --git a/Mathlib/Analysis/NormedSpace/TrivSqZeroExt.lean b/Mathlib/Analysis/NormedSpace/TrivSqZeroExt.lean
@@ -38,6 +38,8 @@ variable (𝕜 : Type*) {R M : Type*}
 
 local notation "tsze" => TrivSqZeroExt
 
+open NormedSpace -- For `exp`.
+
 namespace TrivSqZeroExt
 
 section Topology
diff --git a/Mathlib/Analysis/SpecialFunctions/Exponential.lean b/Mathlib/Analysis/SpecialFunctions/Exponential.lean
@@ -53,7 +53,7 @@ We prove most results for an arbitrary field `𝕂`, and then specialize to `
 -/
 
 
-open Filter IsROrC ContinuousMultilinearMap NormedField Asymptotics
+open Filter IsROrC ContinuousMultilinearMap NormedField NormedSpace Asymptotics
 
 open scoped Nat Topology BigOperators ENNReal
 
@@ -216,14 +216,14 @@ theorem hasDerivAt_exp_zero : HasDerivAt (exp 𝕂) (1 : 𝕂) 0 :=
 
 end DerivROrC
 
-theorem Complex.exp_eq_exp_ℂ : Complex.exp = _root_.exp ℂ := by
+theorem Complex.exp_eq_exp_ℂ : Complex.exp = NormedSpace.exp ℂ := by
   refine' funext fun x => _
   rw [Complex.exp, exp_eq_tsum_div]
   have : CauSeq.IsComplete ℂ norm := Complex.instIsComplete
   exact tendsto_nhds_unique x.exp'.tendsto_limit (expSeries_div_summable ℝ x).hasSum.tendsto_sum_nat
 #align complex.exp_eq_exp_ℂ Complex.exp_eq_exp_ℂ
 
-theorem Real.exp_eq_exp_ℝ : Real.exp = _root_.exp ℝ := by
+theorem Real.exp_eq_exp_ℝ : Real.exp = NormedSpace.exp ℝ := by
   ext x; exact_mod_cast congr_fun Complex.exp_eq_exp_ℂ x
 #align real.exp_eq_exp_ℝ Real.exp_eq_exp_ℝ
 
diff --git a/Mathlib/Analysis/SpecialFunctions/Trigonometric/Series.lean b/Mathlib/Analysis/SpecialFunctions/Trigonometric/Series.lean
@@ -20,6 +20,7 @@ In this file we express trigonometric functions in terms of their series expansi
 * `Real.hasSum_sin`, `Real.sin_eq_tsum`: `Real.sin` as the sum of an infinite series.
 -/
 
+open NormedSpace
 
 open scoped Nat
 
diff --git a/Mathlib/Combinatorics/Derangements/Exponential.lean b/Mathlib/Combinatorics/Derangements/Exponential.lean
@@ -17,7 +17,7 @@ The specific lemma is `numDerangements_tendsto_inv_e`.
 -/
 
 
-open Filter
+open Filter NormedSpace
 
 open scoped BigOperators
 
diff --git a/docs/undergrad.yaml b/docs/undergrad.yaml
@@ -71,7 +71,7 @@ Linear algebra:
     examples: ''
   Exponential:
     endomorphism exponential: ''
-    matrix exponential: 'exp'
+    matrix exponential: 'NormedSpace.exp'
 
 # 2.
 Group Theory:

Original file line number	Diff line number	Diff line change
@@ -19,6 +19,7 @@ These are just restatements of similar statements about `TrivSqZeroExt R M`.
`19`	`19`
`20`	`20`	`-/`
`21`	`21`
	`22`	+open NormedSpace -- For `exp`.
`22`	`23`
`23`	`24`	`namespace DualNumber`
`24`	`25`