From c9fe09849ded34ff118a00d1fc2cebfe2e93eb0b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Thu, 23 Nov 2023 12:56:43 +0000 Subject: [PATCH] =?UTF-8?q?chore:=20Move=20`Data.Nat.Fib`=20=E2=86=92=20`D?= =?UTF-8?q?ata.Nat.Fib.Basic`=20(#8576)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This was postponed to after the Zeckendorf PR. --- Archive/Imo/Imo1981Q3.lean | 2 +- Mathlib.lean | 2 +- .../Algebra/ContinuedFractions/Computation/Approximations.lean | 2 +- Mathlib/Data/Nat/{Fib.lean => Fib/Basic.lean} | 0 Mathlib/Data/Nat/Fib/Zeckendorf.lean | 2 +- Mathlib/Data/Real/GoldenRatio.lean | 2 +- Mathlib/Tactic/NormNum/NatFib.lean | 2 +- 7 files changed, 6 insertions(+), 6 deletions(-) rename Mathlib/Data/Nat/{Fib.lean => Fib/Basic.lean} (100%) diff --git a/Archive/Imo/Imo1981Q3.lean b/Archive/Imo/Imo1981Q3.lean index b9859f454b6b7..90b29784e58c4 100644 --- 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 index ee4e2b336d5fe..f0a6e2bd08109 100644 --- 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 index dd2adc3f9bb42..f8a78987127d1 100644 --- 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 b/Mathlib/Data/Nat/Fib/Basic.lean similarity index 100% rename from Mathlib/Data/Nat/Fib.lean rename to Mathlib/Data/Nat/Fib/Basic.lean diff --git a/Mathlib/Data/Nat/Fib/Zeckendorf.lean b/Mathlib/Data/Nat/Fib/Zeckendorf.lean index d446ad1dce8dd..19afbb61cfeaf 100644 --- 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 index 351769456b0fb..d1b7e21d0f2cf 100644 --- 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 index 55e79c6cd445f..b3ac88c7b46cb 100644 --- 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`