chore: Move Data.Nat.Fib → Data.Nat.Fib.Basic (#8576)

This was postponed to after the Zeckendorf PR.
leanprover-community · Nov 23, 2023 · c9fe098 · c9fe098
1 parent 29bc69a
commit c9fe098
Show file tree

Hide file tree

Showing 7 changed files with 6 additions and 6 deletions.
diff --git a/Archive/Imo/Imo1981Q3.lean b/Archive/Imo/Imo1981Q3.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kevin Lacker
 -/
 import Mathlib.Data.Int.Lemmas
-import Mathlib.Data.Nat.Fib
+import Mathlib.Data.Nat.Fib.Basic
 import Mathlib.Tactic.Linarith
 import Mathlib.Tactic.LinearCombination
 

diff --git a/Mathlib.lean b/Mathlib.lean
@@ -1717,7 +1717,7 @@ import Mathlib.Data.Nat.Factorial.SuperFactorial
 import Mathlib.Data.Nat.Factorization.Basic
 import Mathlib.Data.Nat.Factorization.PrimePow
 import Mathlib.Data.Nat.Factors
-import Mathlib.Data.Nat.Fib
+import Mathlib.Data.Nat.Fib.Basic
 import Mathlib.Data.Nat.Fib.Zeckendorf
 import Mathlib.Data.Nat.ForSqrt
 import Mathlib.Data.Nat.GCD.Basic

diff --git a/Mathlib/Algebra/ContinuedFractions/Computation/Approximations.lean b/Mathlib/Algebra/ContinuedFractions/Computation/Approximations.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kevin Kappelmann
 -/
 import Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating
-import Mathlib.Data.Nat.Fib
+import Mathlib.Data.Nat.Fib.Basic
 import Mathlib.Tactic.Monotonicity
 import Mathlib.Tactic.SolveByElim
 

diff --git a/Mathlib/Data/Nat/Fib.lean → Mathlib/Data/Nat/Fib/Basic.lean b/Mathlib/Data/Nat/Fib.lean → Mathlib/Data/Nat/Fib/Basic.lean
diff --git a/Mathlib/Data/Nat/Fib/Zeckendorf.lean b/Mathlib/Data/Nat/Fib/Zeckendorf.lean
@@ -3,7 +3,7 @@ Copyright (c) 2023 Yaël Dillies. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies
 -/
-import Mathlib.Data.Nat.Fib
+import Mathlib.Data.Nat.Fib.Basic
 
 /-!
 # Zeckendorf's Theorem

diff --git a/Mathlib/Data/Real/GoldenRatio.lean b/Mathlib/Data/Real/GoldenRatio.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Anatole Dedecker, Alexey Soloyev, Junyan Xu
 -/
 import Mathlib.Data.Real.Irrational
-import Mathlib.Data.Nat.Fib
+import Mathlib.Data.Nat.Fib.Basic
 import Mathlib.Data.Nat.PrimeNormNum
 import Mathlib.Data.Fin.VecNotation
 import Mathlib.Algebra.LinearRecurrence

diff --git a/Mathlib/Tactic/NormNum/NatFib.lean b/Mathlib/Tactic/NormNum/NatFib.lean
@@ -3,7 +3,7 @@ Copyright (c) 2023 Kyle Miller. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kyle Miller, Mario Carneiro
 -/
-import Mathlib.Data.Nat.Fib
+import Mathlib.Data.Nat.Fib.Basic
 import Mathlib.Tactic.NormNum
 
 /-! # `norm_num` extension for `Nat.fib`