Fibonacci Divisibility
Let $p$ be an odd prime. Define $f_n$ to be the Fibonacci number (starting with $f_0 = 0$, $f_1 = 1$). Prove that $p$ divides $$\sum_{i=1}^{p-1} f_i \frac {(p-1)!} i.$$
import Mathlib.Data.Nat.Fib.Basic
import Mathlib.Data.Fintype.BigOperators
import Mathlib.Data.Nat.Factorial.Basic
import Mathlib.Order.Interval.Finset.Nat
import Mathlib.Data.Nat.Prime.Defs
theorem solution (p : ℕ) (hp1 : Nat.Prime p) (hp2 : Odd p) :
p ∣ ∑ n ∈ Finset.Icc 1 (p - 1), (Nat.fib n) * (p - 1).factorial / n := sorry
Submit Solution
Login to submit a solution.
Recent Submissions
| # | User | Time (UTC) | Status |
|---|---|---|---|
| 165 | Kitsune | Long time ago | PASSED |