Fibonacci numbers at primes and the Legendre symbol

For every prime p, F(p) ≡ (5/p) (mod p) (with (5/5) = 0). With M the Fibonacci matrix over ZMod p and S = 2M - 1, one has S² = 5; the Frobenius on the commuting matrices gives 2 M^p = 5^{(p-1)/2} S + 1, whose (0, 1) entry is F(p) = 5^{(p-1)/2}, which is the Legendre symbol by Euler's criterion (legendreSym.eq_pow); p = 2 is checked directly.

Main results

• FibLegendre.fib_prime_eq_legendreSym: F(p) = (5/p) in ZMod p for every prime p

References

• E. Lucas, Théorie des fonctions numériques simplement périodiques, Amer. J. Math. 1 (1878).
• The companion divisibility p ∣ F(p − (5/p)) is in facebookresearch/atlas-lean, MathlibExt/NumberTheory/Recurrences/FibonacciPrimeDivisibility.lean.

theorem FibLegendre.fib_prime_eq_legendreSym (p : ℕ) [Fact (Nat.Prime p)] : ↑↑(Nat.fib p) = ↑(legendreSym p 5)

Fibonacci numbers at primes. For every prime p, F(p) ≡ (5/p) (mod p), with (5/p) the Legendre symbol (0 for p = 5).