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.