Commit 2023-01-19 17:01 4260082a

View on Github →

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

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Nat/Fib.lean

added def Nat.fastFib

added def Nat.fastFibAux

added theorem Nat.fast_fib_aux_bit_ff

added theorem Nat.fast_fib_aux_bit_tt

added theorem Nat.fast_fib_aux_eq

added theorem Nat.fast_fib_eq

added def Nat.fib

added theorem Nat.fib_add

added theorem Nat.fib_add_two

added theorem Nat.fib_add_two_strict_mono

added theorem Nat.fib_add_two_sub_fib_add_one

added theorem Nat.fib_bit0

added theorem Nat.fib_bit0_succ

added theorem Nat.fib_bit1

added theorem Nat.fib_bit1_succ

added theorem Nat.fib_coprime_fib_succ

added theorem Nat.fib_dvd

added theorem Nat.fib_gcd

added theorem Nat.fib_le_fib_succ

added theorem Nat.fib_lt_fib_succ

added theorem Nat.fib_mono

added theorem Nat.fib_one

added theorem Nat.fib_pos

added theorem Nat.fib_succ_eq_succ_sum

added theorem Nat.fib_succ_eq_sum_choose

added theorem Nat.fib_two

added theorem Nat.fib_two_mul

added theorem Nat.fib_two_mul_add_one

added theorem Nat.fib_zero

added theorem Nat.gcd_fib_add_mul_self

added theorem Nat.gcd_fib_add_self

added theorem Nat.le_fib_self

added def NormNum.IsFibAux

added theorem NormNum.is_fib_aux_bit0

added theorem NormNum.is_fib_aux_bit0_done

added theorem NormNum.is_fib_aux_bit1

added theorem NormNum.is_fib_aux_bit1_done

added theorem NormNum.is_fib_aux_one

Created Mathlib/Init/Data/Nat/GCD.lean

added def Nat.Coprime

added theorem Nat.gcd_def