Skip to content

Commit 4260082

Browse files
feat: port Data.Nat.Fib (#1644)
Co-authored-by: ChrisHughes24 <chrishughes24@gmail.com>
1 parent 9c7b0eb commit 4260082

File tree

3 files changed

+582
-0
lines changed

3 files changed

+582
-0
lines changed

Mathlib.lean

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -365,6 +365,7 @@ import Mathlib.Data.Nat.Choose.Dvd
365365
import Mathlib.Data.Nat.Dist
366366
import Mathlib.Data.Nat.EvenOddRec
367367
import Mathlib.Data.Nat.Factorial.Basic
368+
import Mathlib.Data.Nat.Fib
368369
import Mathlib.Data.Nat.ForSqrt
369370
import Mathlib.Data.Nat.GCD.Basic
370371
import Mathlib.Data.Nat.GCD.BigOperators
@@ -521,6 +522,7 @@ import Mathlib.Init.Data.List.Instances
521522
import Mathlib.Init.Data.List.Lemmas
522523
import Mathlib.Init.Data.Nat.Basic
523524
import Mathlib.Init.Data.Nat.Bitwise
525+
import Mathlib.Init.Data.Nat.GCD
524526
import Mathlib.Init.Data.Nat.Lemmas
525527
import Mathlib.Init.Data.Nat.Notation
526528
import Mathlib.Init.Data.Ordering.Basic

0 commit comments

Comments
 (0)