Commit 2026-02-04 00:38 5b38ccdf

View on Github →

chore(Nat/Fib/Basic): fix names and csimp (#34810) and add a csimp lemma to connect the existing Nat.fastFib.

Estimated changes

Modified Mathlib/Data/Nat/Fib/Basic.lean

added theorem Nat.fastFibAux_bit_false

added theorem Nat.fastFibAux_bit_true

added theorem Nat.fastFibAux_eq

added theorem Nat.fastFib_eq

deleted theorem Nat.fast_fib_aux_bit_ff

deleted theorem Nat.fast_fib_aux_bit_tt

deleted theorem Nat.fast_fib_aux_eq

deleted theorem Nat.fast_fib_eq

added theorem Nat.fib_eq_fastFib