Fibonomial coefficients
TheoremLifting the exponent for Fibonacci numbers#✓fully proved
Let \(p\) be an odd prime and \(m \ge 1\) an integer such that \(p\) divides the Fibonacci number \(F_m\), and write \(v_p\) for the \(p\)-adic valuation. Then \(v_p(F_{mj}) = v_p(F_m) + v_p(j)\) for every integer \(j \ge 1\).
theorem padicValNat_fib_mul (p : ℕ) [Fact (Nat.Prime p)] (hp2 : p ≠ 2)
(m : ℕ) (hm : 1 ≤ m) (hdvd : p ∣ Nat.fib m) (j : ℕ) (hj : 1 ≤ j) :
padicValNat p (Nat.fib (m * j)) = padicValNat p (Nat.fib m) + padicValNat p j
TheoremVanishing \(p\)-adic valuation of Fibonomial coefficients at prime powers#✓fully proved
Let \(p\) be a prime with \(p \ne 2\) and \(p \ne 5\), and let \(a, b\) be integers with \(0 < a \le b\) such that \(p \equiv \pm 1 \pmod 5\) or \(a \equiv b \pmod 2\). Write \(F_n\) for the \(n\)-th Fibonacci number and \(F_n! = F_1 F_2 \cdots F_n\) for the Fibonacci factorial, with \(F_0! = 1\). Then the \(p\)-adic valuation of the Fibonomial coefficient
where the quotient is taken by division of natural numbers, is \(0\).
theorem fibonomial_primePower_padicVal_eq_zero
(p a b : ℕ) (hp : p.Prime) (hp2 : p ≠ 2) (hp5 : p ≠ 5)
(ha : 0 < a) (hab : a ≤ b)
(hbranch : (p % 5 = 1 ∨ p % 5 = 4) ∨ a % 2 = b % 2) :
padicValNat p
((∏ i ∈ Finset.range (p ^ b), Nat.fib (i + 1)) /
((∏ i ∈ Finset.range (p ^ a), Nat.fib (i + 1)) *
∏ i ∈ Finset.range (p ^ b - p ^ a), Nat.fib (i + 1))) = 0
Sources
- Phunphayap–Pongsriiam, Example
rem18, equationeq1remark2.
Uses 2
TheoremKimball–Webb congruence for Fibonomial coefficients modulo \(p^3\)#✓fully proved
Let \(F_n\) be the Fibonacci numbers, with \(F_1 = F_2 = 1\), and write \(F_n! = F_1 F_2 \cdots F_n\), with \(F_0! = 1\). Let \(p \ge 7\) be a prime and \(\varepsilon \in \{1, -1\}\), and suppose that \(\rho = p - \varepsilon\) is the rank of appearance of \(p\), that is, \(p \mid F_\rho\) and \(p \nmid F_m\) for \(0 < m < \rho\). Then for every natural number \(k\) the Fibonomial coefficient
is congruent to \(\varepsilon^k\) modulo \(p^3\).
The quotient is taken in the natural numbers; it is exact because Fibonomial coefficients are integers. This is the Fibonacci case only, not Ballot's general theorem for Lucasnomial coefficients.
theorem fibonomial_prime_cube_congr :
∀ (p rho : ℕ) (ε : ℤ) (k : ℕ), Nat.Prime p → 7 ≤ p →
(ε = 1 ∨ ε = -1) → (rho : ℤ) = (p : ℤ) - ε → Nat.fib rho % p = 0 →
(∀ m : ℕ, 0 < m → m < rho → ¬ p ∣ Nat.fib m) →
Int.ModEq ((p : ℤ) ^ 3)
(((Finset.prod (Finset.range ((k + 1) * rho - 1)) (fun i => Nat.fib (i + 1)) /
(Finset.prod (Finset.range (rho - 1)) (fun i => Nat.fib (i + 1)) *
Finset.prod (Finset.range (k * rho)) (fun i => Nat.fib (i + 1)))) : ℕ) : ℤ)
(ε ^ k)
Sources
- Christian Ballot, The Congruence of Wolstenholme for Generalized Binomial Coefficients Related to Lucas Sequences, Journal of Integer Sequences 18 (2015), Article 15.5.4, https://cs.uwaterloo.ca/journals/JIS/VOL18/Ballot/ballot14.tex, Theorem
thm:KW(rewriting Lemma 3 of Kimball and Webb), equationeq:Fib, lines 144-150.
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.