Lucas sequences and primitive divisors

General Lucas sequences U_n, V_n, Lucas pairs, divisibility, Bang–Zsigmondy and primitive-divisor theorems, Fibonacci prime divisibility.

• Lucas sequences
• Composite terms of shifted Lucas sequences
• Primitive divisors
• Divisibility properties of Lucas sequences
• Large Zsigmondy primes
• Zsigmondy's theorem

TheoremFibonacci prime divisibility#✓fully proved

Let \(p\) be a prime with \(p > 2\) and \(p \ne 5\), and let \(\left(\frac{5}{p}\right)\) be the Legendre symbol of \(5\) modulo \(p\). Then \(p\) divides the Fibonacci number \(F_{p-1}\) if \(\left(\frac{5}{p}\right) = 1\), and \(p\) divides the Fibonacci number \(F_{p+1}\) otherwise. Since \(\left(\frac{5}{p}\right) = \pm 1\), this says that \(p\) divides \(F_{p - \left(\frac{5}{p}\right)}\).

theorem fib_prime_dvd_fib_of_legendre_sub
    (p : ℕ) [Fact (Nat.Prime p)] (h5 : p ≠ 5) (h2 : 2 < p) :
    p ∣ Nat.fib (if legendreSym p 5 = 1 then p - 1 else p + 1)

Sources

• Phakhinkon Phunphayap and Prapanpong Pongsriiam, "Explicit Formulas for the p-adic Valuations of Fibonomial Coefficients," Journal of Integer Sequences 21 (2018), Article 18.3.1, Lemma, item (i), lines 166–169, https://cs.uwaterloo.ca/journals/JIS/VOL21/Pongsriiam/pong12.tex

Used by 2

Used byFulton–Morris theorem on Pisano periods equal to the modulus · Vanishing \(p\)-adic valuation of Fibonomial coefficients at prime powers

TheoremThe \(5\)-adic valuation of Fibonacci numbers#✓fully proved

Writing \(F_n\) for the \(n\)-th Fibonacci number and \(v_5\) for the \(5\)-adic valuation, \(v_5(F_n) = v_5(n)\) for every integer \(n \ge 1\).

theorem lengyel_fibonacci_five_adic
    (n : ℕ) (hn : 1 ≤ n) :
    padicValNat 5 (Nat.fib n) = padicValNat 5 n

Sources

• Fatehizadeh–Yaqubi, Lemma Leg1, citing Lengyel (1995). The source prints n ≥ 0, but its p-adic valuation is defined for positive integers, so this formalizes the audited 1 ≤ n restriction. Only the 5-adic clause is formalized; the source's separate 2-adic and 3-adic clauses are out of scope.

Used by 1

Used byFulton–Morris theorem on Pisano periods equal to the modulus

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.