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
Used by 2

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

\[\binom{p^b}{p^a}_F = \frac{F_{p^b}!}{F_{p^a}! \, F_{p^b - p^a}!},\]

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, equation eq1remark2.
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

\[\binom{(k+1)\rho - 1}{\rho - 1}_F = \frac{F_{(k+1)\rho - 1}!}{F_{\rho - 1}!\, F_{k\rho}!}\]

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), equation eq:Fib, lines 144-150.
3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.