fix imports

leanprover-community · Jan 26, 2025 · 6f6e836 · 6f6e836
1 parent 72e58d9
commit 6f6e836
Show file tree

Hide file tree

Showing 8 changed files with 8 additions and 7 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -2499,6 +2499,7 @@ import Mathlib.Data.Complex.FiniteDimensional
 import Mathlib.Data.Complex.Module
 import Mathlib.Data.Complex.Order
 import Mathlib.Data.Complex.Orientation
+import Mathlib.Data.Complex.Trigonometric
 import Mathlib.Data.Countable.Basic
 import Mathlib.Data.Countable.Defs
 import Mathlib.Data.Countable.Small

diff --git a/Mathlib/Analysis/Complex/Basic.lean b/Mathlib/Analysis/Complex/Basic.lean
@@ -5,7 +5,7 @@ Authors: Sébastien Gouëzel
 -/
 import Mathlib.Data.Complex.Module
 import Mathlib.Data.Complex.Order
-import Mathlib.Data.Complex.Exponential
+import Mathlib.Data.Complex.Trigonometric
 import Mathlib.Analysis.RCLike.Basic
 import Mathlib.Topology.Algebra.InfiniteSum.Field
 import Mathlib.Topology.Algebra.InfiniteSum.Module

diff --git a/Mathlib/Analysis/SpecialFunctions/Log/ERealExp.lean b/Mathlib/Analysis/SpecialFunctions/Log/ERealExp.lean
@@ -3,7 +3,7 @@ Copyright (c) 2024 Rémy Degenne. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Pietro Monticone, Rémy Degenne, Lorenzo Luccioli
 -/
-import Mathlib.Data.Complex.Exponential
+import Mathlib.Data.Complex.Trigonometric
 import Mathlib.Data.Real.EReal
 
 /-!

diff --git a/Mathlib/Analysis/SpecialFunctions/Trigonometric/Chebyshev.lean b/Mathlib/Analysis/SpecialFunctions/Trigonometric/Chebyshev.lean
@@ -3,7 +3,7 @@ Copyright (c) 2020 Johan Commelin. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johan Commelin
 -/
-import Mathlib.Data.Complex.Exponential
+import Mathlib.Data.Complex.Trigonometric
 import Mathlib.Data.Complex.Module
 import Mathlib.RingTheory.Polynomial.Chebyshev
 

diff --git a/Mathlib/Data/Complex/ExponentialBounds.lean b/Mathlib/Data/Complex/ExponentialBounds.lean
@@ -3,7 +3,7 @@ Copyright (c) 2020 Joseph Myers. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, Joseph Myers
 -/
-import Mathlib.Data.Complex.Exponential
+import Mathlib.Data.Complex.Trigonometric
 import Mathlib.Analysis.SpecialFunctions.Log.Deriv
 
 /-!

diff --git a/Mathlib/Tactic/FunProp.lean b/Mathlib/Tactic/FunProp.lean
@@ -37,7 +37,7 @@ example (y : ℝ) (hy : y ≠ 0) : ContinuousAt (fun x : ℝ => 1/x) y := by fun
 **Basic debugging:**
 The most common issue is that a function is missing the appropriate theorem. For example:
 ```lean
-import Mathlib.Data.Complex.Exponential
+import Mathlib.Data.Complex.Trigonometric
 example : Continuous (fun x : ℝ => x * Real.sin x) := by fun_prop
 ```
 Fails with the error:

diff --git a/MathlibTest/Recall.lean b/MathlibTest/Recall.lean
@@ -1,7 +1,7 @@
 import Mathlib.Tactic.Recall
 import Mathlib.Analysis.Calculus.Deriv.Basic
 import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
-import Mathlib.Data.Complex.Exponential
+import Mathlib.Data.Complex.Trigonometric
 
 set_option linter.style.setOption false
 -- Remark: When the test is run by make/CI, this option is not set, so we set it here.

diff --git a/MathlibTest/positivity.lean b/MathlibTest/positivity.lean
@@ -1,5 +1,5 @@
 import Mathlib.Tactic.Positivity
-import Mathlib.Data.Complex.Exponential
+import Mathlib.Data.Complex.Trigonometric
 import Mathlib.Data.Real.Sqrt
 import Mathlib.Analysis.Normed.Group.Basic
 import Mathlib.Analysis.SpecialFunctions.Pow.Real