feat: port Data.Nat.Fib (#1644)

Co-authored-by: ChrisHughes24 <chrishughes24@gmail.com>
leanprover-community · Jan 19, 2023 · 4260082 · 4260082
1 parent 9c7b0eb
commit 4260082
Show file tree

Hide file tree

Showing 3 changed files with 582 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -365,6 +365,7 @@ import Mathlib.Data.Nat.Choose.Dvd
 import Mathlib.Data.Nat.Dist
 import Mathlib.Data.Nat.EvenOddRec
 import Mathlib.Data.Nat.Factorial.Basic
+import Mathlib.Data.Nat.Fib
 import Mathlib.Data.Nat.ForSqrt
 import Mathlib.Data.Nat.GCD.Basic
 import Mathlib.Data.Nat.GCD.BigOperators
@@ -521,6 +522,7 @@ import Mathlib.Init.Data.List.Instances
 import Mathlib.Init.Data.List.Lemmas
 import Mathlib.Init.Data.Nat.Basic
 import Mathlib.Init.Data.Nat.Bitwise
+import Mathlib.Init.Data.Nat.GCD
 import Mathlib.Init.Data.Nat.Lemmas
 import Mathlib.Init.Data.Nat.Notation
 import Mathlib.Init.Data.Ordering.Basic