Skip to content

Commit f1ab97a

Browse files
committed
Restored Chebyshev.lean, and moved new files to a new folder, "ChebyshevReal"
1 parent b2856e2 commit f1ab97a

4 files changed

Lines changed: 5 additions & 5 deletions

File tree

Mathlib/Analysis/SpecialFunctions/Trigonometric/Chebyshev.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@ Authors: Johan Commelin
55
-/
66
import Mathlib.Data.Complex.Trigonometric
77
import Mathlib.Data.Complex.Module
8-
import Mathlib.RingTheory.Polynomial.Chebyshev.Basic
8+
import Mathlib.RingTheory.Polynomial.Chebyshev
99

1010
/-!
1111
# Multiple angle formulas in terms of Chebyshev polynomials
File renamed without changes.

Mathlib/RingTheory/Polynomial/Chebyshev/Real.lean renamed to Mathlib/RingTheory/Polynomial/ChebyshevReal/Basic.lean

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,9 @@
11
/-
2-
Copyright (c) 2020 Johan Commelin. All rights reserved.
2+
Copyright (c) 2020 Yuval Filmus. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Yuval Filmus
55
-/
6-
import Mathlib.RingTheory.Polynomial.Chebyshev.Basic
6+
import Mathlib.RingTheory.Polynomial.Chebyshev
77
import Mathlib.Data.Real.Basic
88
import Mathlib.Algebra.Polynomial.Roots
99
import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Mathlib/RingTheory/Polynomial/Chebyshev/Monic.lean renamed to Mathlib/RingTheory/Polynomial/ChebyshevReal/Monic.lean

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,9 @@
11
/-
2-
Copyright (c) 2020 Johan Commelin. All rights reserved.
2+
Copyright (c) 2020 Yuval Filmus. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Yuval Filmus
55
-/
6-
import Mathlib.RingTheory.Polynomial.Chebyshev.Real
6+
import Mathlib.RingTheory.Polynomial.ChebyshevReal.Basic
77
import Mathlib.LinearAlgebra.Lagrange
88
import Mathlib.Topology.Algebra.Polynomial
99

0 commit comments

Comments
 (0)