Revert some of the exp changes. Others are actually good, in my opinion.

Mathlib/Analysis/Calculus/FDeriv/Basic.lean

@@ -71,7 +71,7 @@ not vanish, as in
 example (x : ℝ) (h : 1 + sin x ≠ 0) : DifferentiableAt ℝ (fun x ↦ exp x / (1 + sin x)) x :=
 by simp [h]
 ```
-Of course, these examples only work once `NormedSpace.exp`, `cos` and `sin` have been shown to be
+Of course, these examples only work once `exp`, `cos` and `sin` have been shown to be
 differentiable, in `Analysis.SpecialFunctions.Trigonometric`.
 
 The simplifier is not set up to compute the Fréchet derivative of maps (as these are in general
@@ -102,7 +102,7 @@ many lemmas with the `simp` attribute, for instance those saying that the sum of
 functions is differentiable, as well as their product, their cartesian product, and so on. A notable
 exception is the chain rule: we do not mark as a simp lemma the fact that, if `f` and `g` are
 differentiable, then their composition also is: `simp` would always be able to match this lemma,
-by taking `f` or `g` to be the identity. Instead, for every reasonable function (say, `NormedSpace.exp`),
+by taking `f` or `g` to be the identity. Instead, for every reasonable function (say, `exp`),
 we add a lemma that if `f` is differentiable then so is `(fun x ↦ exp (f x))`. This means adding
 some boilerplate lemmas, but these can also be useful in their own right.
 

Mathlib/Analysis/NormedSpace/Exponential.lean

@@ -19,7 +19,7 @@ In this file, we define `exp 𝕂 : 𝔸 → 𝔸`, the exponential map in a top
 field `𝕂`.
 
 While for most interesting results we need `𝔸` to be normed algebra, we do not require this in the
-definition in order to make `NormedSpace.exp` independent of a particular choice of norm. The definition also
+definition in order to make `exp` independent of a particular choice of norm. The definition also
 does not require that `𝔸` be complete, but we need to assume it for most results.
 
 We then prove some basic results, but we avoid importing derivatives here to minimize dependencies.
@@ -52,14 +52,15 @@ We prove most result for an arbitrary field `𝕂`, and then specialize to `𝕂
 - `NormedSpace.exp_neg` : if `𝔸` is a division ring, then we have `exp 𝕂 (-x) = (exp 𝕂 x)⁻¹`.
 - `exp_sum_of_commute` : the analogous result to `NormedSpace.exp_add_of_commute` for `Finset.sum`.
 - `exp_sum` : the analogous result to `NormedSpace.exp_add` for `Finset.sum`.
-- `NormedSpace.exp_nsmul` : repeated addition in the domain corresponds to repeated multiplication in the
-  codomain.
-- `NormedSpace.exp_zsmul` : repeated addition in the domain corresponds to repeated multiplication in the
-  codomain.
+- `NormedSpace.exp_nsmul` : repeated addition in the domain corresponds to
+  repeated multiplication in the codomain.
+- `NormedSpace.exp_zsmul` : repeated addition in the domain corresponds to
+  repeated multiplication in the codomain.
 
 ### Other useful compatibility results
 
-- `NormedSpace.exp_eq_exp` : if `𝔸` is a normed algebra over two fields `𝕂` and `𝕂'`, then `exp 𝕂 = exp 𝕂' 𝔸`
+- `NormedSpace.exp_eq_exp` : if `𝔸` is a normed algebra over two fields `𝕂` and `𝕂'`,
+  then `exp 𝕂 = exp 𝕂' 𝔸`
 
 ### Notes
 
@@ -78,7 +79,7 @@ open Real
 This is because `exp x` tries the `NormedSpace.exp` function defined here,
 and generates a slow coercion search from `Real` to `Type`, to fit the first argument here.
 We will resolve this slow coercion separately,
-but we want to move `NormedSpace.exp` out of the root namespace in any case to avoid this ambiguity.
+but we want to move `exp` out of the root namespace in any case to avoid this ambiguity.
 
 In the long term is may be possible to replace `Real.exp` and `Complex.exp` with this one.
 
@@ -330,7 +331,7 @@ theorem invOf_exp_of_mem_ball [CharZero 𝕂] {x : 𝔸}
   letI := invertibleExpOfMemBall hx; convert (rfl : ⅟ (exp 𝕂 x) = _)
 #align inv_of_exp_of_mem_ball NormedSpace.invOf_exp_of_mem_ball
 
-/-- Any continuous ring homomorphism commutes with `NormedSpace.exp`. -/
+/-- Any continuous ring homomorphism commutes with `exp`. -/
 theorem map_exp_of_mem_ball {F} [FunLike F 𝔸 𝔹] [RingHomClass F 𝔸 𝔹] (f : F) (hf : Continuous f)
     (x : 𝔸) (hx : x ∈ EMetric.ball (0 : 𝔸) (expSeries 𝕂 𝔸).radius) :
     f (exp 𝕂 x) = exp 𝕂 (f x) := by

Mathlib/Analysis/NormedSpace/MatrixExponential.lean

@@ -15,25 +15,26 @@ import Mathlib.Topology.UniformSpace.Matrix
 /-!
 # Lemmas about the matrix exponential
 
-In this file, we provide results about `NormedSpace.exp` on `Matrix`s over a topological or normed algebra.
-Note that generic results over all topological spaces such as `NormedSpace.exp_zero` can be used on matrices
-without issue, so are not repeated here. The topological results specific to matrices are:
+In this file, we provide results about `exp` on `Matrix`s over a topological or normed algebra.
+Note that generic results over all topological spaces such as `NormedSpace.exp_zero`
+can be used on matrices without issue, so are not repeated here.
+The topological results specific to matrices are:
 
 * `Matrix.exp_transpose`
 * `Matrix.exp_conjTranspose`
 * `Matrix.exp_diagonal`
 * `Matrix.exp_blockDiagonal`
 * `Matrix.exp_blockDiagonal'`
 
-Lemmas like `NormedSpace.exp_add_of_commute` require a canonical norm on the type; while there are multiple
-sensible choices for the norm of a `Matrix` (`Matrix.normedAddCommGroup`,
+Lemmas like `NormedSpace.exp_add_of_commute` require a canonical norm on the type;
+while there are multiple sensible choices for the norm of a `Matrix` (`Matrix.normedAddCommGroup`,
 `Matrix.frobeniusNormedAddCommGroup`, `Matrix.linftyOpNormedAddCommGroup`), none of them
 are canonical. In an application where a particular norm is chosen using
-`attribute [local instance]`, then the usual lemmas about `NormedSpace.exp` are fine. When choosing a norm is
-undesirable, the results in this file can be used.
+`attribute [local instance]`, then the usual lemmas about `NormedSpace.exp` are fine.
+When choosing a norm is undesirable, the results in this file can be used.
 
-In this file, we copy across the lemmas about `NormedSpace.exp`, but hide the requirement for a norm inside the
-proof.
+In this file, we copy across the lemmas about `NormedSpace.exp`,
+but hide the requirement for a norm inside the proof.
 
 * `Matrix.exp_add_of_commute`
 * `Matrix.exp_sum_of_commute`
@@ -62,7 +63,7 @@ results for general rings are instead stated about `Ring.inverse`:
 
 open scoped Matrix BigOperators
 
-open NormedSpace -- For `NormedSpace.exp`.
+open NormedSpace -- For `exp`.
 
 variable (𝕂 : Type*) {m n p : Type*} {n' : m → Type*} {𝔸 : Type*}
 

Mathlib/Analysis/NormedSpace/TrivSqZeroExt.lean

@@ -54,7 +54,7 @@ variable (𝕜 : Type*) {S R M : Type*}
 
 local notation "tsze" => TrivSqZeroExt
 
-open NormedSpace -- For `NormedSpace.exp`.
+open NormedSpace -- For `exp`.
 
 namespace TrivSqZeroExt
 
@@ -322,7 +322,7 @@ variable [BoundedSMul R M] [BoundedSMul Rᵐᵒᵖ M] [SMulCommClass R Rᵐᵒ
 variable [IsScalarTower 𝕜 R M] [IsScalarTower 𝕜 Rᵐᵒᵖ M]
 variable [CompleteSpace R] [CompleteSpace M]
 
--- Evidence that we have sufficient instances on `tsze R N` to make `NormedSpace.exp_add_of_commute` usable
+-- Evidence that we have sufficient instances on `tsze R N` to make `exp_add_of_commute` usable
 example (a b : tsze R M) (h : Commute a b) : exp 𝕜 (a + b) = exp 𝕜 a * exp 𝕜 b :=
   exp_add_of_commute h
 

Mathlib/Analysis/SpecialFunctions/Complex/Log.lean

@@ -11,7 +11,7 @@ import Mathlib.Analysis.SpecialFunctions.Log.Basic
 /-!
 # The complex `log` function
 
-Basic properties, relationship with `NormedSpace.exp`.
+Basic properties, relationship with `exp`.
 -/
 
 
@@ -23,7 +23,7 @@ open Set Filter Bornology
 
 open scoped Real Topology ComplexConjugate
 
-/-- Inverse of the `NormedSpace.exp` function. Returns values such that `(log x).im > - π` and `(log x).im ≤ π`.
+/-- Inverse of the `exp` function. Returns values such that `(log x).im > - π` and `(log x).im ≤ π`.
   `log 0 = 0`-/
 -- Porting note: @[pp_nodot] does not exist in mathlib4
 noncomputable def log (x : ℂ) : ℂ :=

Mathlib/Analysis/SpecificLimits/Normed.lean

@@ -768,9 +768,9 @@ end
 ### Factorial
 -/
 
-/-- The series `∑' n, x ^ n / n!` is summable of any `x : ℝ`. See also `NormedSpace.expSeries_div_summable`
-for a version that also works in `ℂ`, and `NormedSpace.expSeries_summable'` for a version that works in
-any normed algebra over `ℝ` or `ℂ`. -/
+/-- The series `∑' n, x ^ n / n!` is summable of any `x : ℝ`. See also `expSeries_div_summable`
+for a version that also works in `ℂ`, and `NormedSpace.expSeries_summable'` for a version
+that works inany normed algebra over `ℝ` or `ℂ`. -/
 theorem Real.summable_pow_div_factorial (x : ℝ) : Summable (fun n ↦ x ^ n / n ! : ℕ → ℝ) := by
   -- We start with trivial estimates
   have A : (0 : ℝ) < ⌊‖x‖⌋₊ + 1 := zero_lt_one.trans_le (by simp)