Skip to content

Commit e779c77

Browse files
committed
chore(Data/Complex/Exponential): split trig functions to new file (#21075)
This PR splits Data/Complex/Exponential.lean into a new Trigonometric.lean file, addressing an instance of a long file linter trigger.
1 parent de46196 commit e779c77

File tree

8 files changed

+959
-887
lines changed

8 files changed

+959
-887
lines changed

Mathlib.lean

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2501,6 +2501,7 @@ import Mathlib.Data.Complex.FiniteDimensional
25012501
import Mathlib.Data.Complex.Module
25022502
import Mathlib.Data.Complex.Order
25032503
import Mathlib.Data.Complex.Orientation
2504+
import Mathlib.Data.Complex.Trigonometric
25042505
import Mathlib.Data.Countable.Basic
25052506
import Mathlib.Data.Countable.Defs
25062507
import Mathlib.Data.Countable.Small

Mathlib/Analysis/Complex/Basic.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@ Authors: Sébastien Gouëzel
55
-/
66
import Mathlib.Data.Complex.Module
77
import Mathlib.Data.Complex.Order
8-
import Mathlib.Data.Complex.Exponential
8+
import Mathlib.Data.Complex.Trigonometric
99
import Mathlib.Analysis.RCLike.Basic
1010
import Mathlib.Topology.Algebra.InfiniteSum.Field
1111
import Mathlib.Topology.Algebra.InfiniteSum.Module

Mathlib/Analysis/SpecialFunctions/Trigonometric/Chebyshev.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ Copyright (c) 2020 Johan Commelin. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Johan Commelin
55
-/
6-
import Mathlib.Data.Complex.Exponential
6+
import Mathlib.Data.Complex.Trigonometric
77
import Mathlib.Data.Complex.Module
88
import Mathlib.RingTheory.Polynomial.Chebyshev
99

0 commit comments

Comments
 (0)