fix: deduplicate and make exp notation scoped (#7297)

[Zulip](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/duplicate.20notation.20cexp)
leanprover-community · Sep 21, 2023 · 08c9bdd · 08c9bdd
1 parent 2e62146
commit 08c9bdd
Show file tree

Hide file tree

Showing 3 changed files with 6 additions and 6 deletions.
diff --git a/Mathlib/Analysis/SpecialFunctions/Gamma/Beta.lean b/Mathlib/Analysis/SpecialFunctions/Gamma/Beta.lean
@@ -55,8 +55,6 @@ section BetaIntegral
 
 namespace Complex
 
-notation "cexp" => Complex.exp
-
 /-- The Beta function `Β (u, v)`, defined as `∫ x:ℝ in 0..1, x ^ (u - 1) * (1 - x) ^ (v - 1)`. -/
 noncomputable def betaIntegral (u v : ℂ) : ℂ :=
   ∫ x : ℝ in (0)..1, (x : ℂ) ^ (u - 1) * (1 - (x : ℂ)) ^ (v - 1)

diff --git a/Mathlib/Analysis/SpecialFunctions/Gaussian.lean b/Mathlib/Analysis/SpecialFunctions/Gaussian.lean
@@ -47,10 +47,6 @@ open scoped Real Topology FourierTransform
 
 open Complex hiding exp continuous_exp abs_of_nonneg sq_abs
 
-notation "cexp" => Complex.exp
-
-notation "rexp" => Real.exp
-
 theorem exp_neg_mul_sq_isLittleO_exp_neg {b : ℝ} (hb : 0 < b) :
     (fun x : ℝ => exp (-b * x ^ 2)) =o[atTop] fun x : ℝ => exp (-x) := by
   have A : (fun x : ℝ => -x - -b * x ^ 2) = fun x => x * (b * x + -1) := by ext x; ring

diff --git a/Mathlib/Data/Complex/Exponential.lean b/Mathlib/Data/Complex/Exponential.lean
@@ -416,6 +416,9 @@ def tanh (z : ℂ) : ℂ :=
   sinh z / cosh z
 #align complex.tanh Complex.tanh
 
+/-- scoped notation for the complex exponential function -/
+scoped notation "cexp" => Complex.exp
+
 end
 
 end Complex
@@ -469,6 +472,9 @@ nonrec def tanh (x : ℝ) : ℝ :=
   (tanh x).re
 #align real.tanh Real.tanh
 
+/-- scoped notation for the real exponential function -/
+scoped notation "rexp" => Real.exp
+
 end
 
 end Real