Commit 2025-11-26 13:56 0bee8dd0

View on Github →

chore(Data/Int/Fib): add fib_neg (#32107) Forgot to add Int.fib_neg:

theorem fib_neg (n : ℤ) : fib (-n) = if Even n then -fib n else fib n := by

Also changes Int.fib_gcd to Int.gcd_fib and gets rid of the unnecessary coercions.

Estimated changes

deleted theorem Int.fib_gcd
added theorem Int.fib_neg
added theorem Int.gcd_fib