Commit 2025-11-25 16:28 9011acf6

View on Github →

feat(Data/Int): define Int.fib, the Fibonacci numbers on the integers (#30936) We define Int.fib, the integer version of Nat.fib, which satisfies Int.fib 0 = 0, Int.fib 1 = 1, and Int.fib (n + 2) = Int.fib n + Int.fib (n + 1).

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Int/Fib.lean

added theorem Int.coe_fib_neg

added def Int.fib

added theorem Int.fib_add

added theorem Int.fib_add_one

added theorem Int.fib_add_two

added theorem Int.fib_dvd

added theorem Int.fib_eq_fib_add_two_sub_fib_add_one

added theorem Int.fib_eq_zero

added theorem Int.fib_gcd

added theorem Int.fib_natCast

added theorem Int.fib_neg_natCast

added theorem Int.fib_neg_one

added theorem Int.fib_neg_two

added theorem Int.fib_of_nonneg

added theorem Int.fib_of_odd

added theorem Int.fib_one

added theorem Int.fib_two

added theorem Int.fib_two_mul

added theorem Int.fib_two_mul_add_one

added theorem Int.fib_two_mul_add_one_eq_natFib_natAbs

added theorem Int.fib_two_mul_add_one_pos

added theorem Int.fib_two_mul_add_two

added theorem Int.fib_zero