Lucas's theorem

This file contains a proof of Lucas's theorem about binomial coefficients, which says that for primes p, n choose k is congruent to product of n_i choose k_i modulo p, where n_i and k_i are the base-p digits of n and k, respectively.

Main statements

• lucas_theorem: the binomial coefficient n choose k is congruent to the product of n_i choose k_i modulo p, where n_i and k_i are the base-p digits of n and k, respectively.

theorem Choose.choose_modEq_choose_mod_mul_choose_div {n : ℕ} {k : ℕ} {p : ℕ} [Fact (Nat.Prime p)] : ↑(n.choose k) ≡ ↑((n % p).choose (k % p)) * ↑((n / p).choose (k / p)) [ZMOD ↑p]

For primes p, choose n k is congruent to choose (n % p) (k % p) * choose (n / p) (k / p) modulo p. Also see choose_modEq_choose_mod_mul_choose_div_nat for the version with MOD.

theorem Choose.choose_modEq_choose_mod_mul_choose_div_nat {n : ℕ} {k : ℕ} {p : ℕ} [Fact (Nat.Prime p)] : n.choose k ≡ (n % p).choose (k % p) * (n / p).choose (k / p) [MOD p]

For primes p, choose n k is congruent to choose (n % p) (k % p) * choose (n / p) (k / p) modulo p. Also see choose_modEq_choose_mod_mul_choose_div for the version with ZMOD.

theorem Choose.choose_modEq_choose_mul_prod_range_choose {n : ℕ} {k : ℕ} {p : ℕ} [Fact (Nat.Prime p)] (a : ℕ) : ↑(n.choose k) ≡ ↑((n / p ^ a).choose (k / p ^ a)) * ↑(∏ i ∈ Finset.range a, (n / p ^ i % p).choose (k / p ^ i % p)) [ZMOD ↑p]

For primes p, choose n k is congruent to the product of choose (⌊n / p ^ i⌋ % p) (⌊k / p ^ i⌋ % p) over i < a, multiplied by choose (⌊n / p ^ a⌋) (⌊k / p ^ a⌋), modulo p.

theorem Choose.choose_modEq_prod_range_choose {n : ℕ} {k : ℕ} {p : ℕ} [Fact (Nat.Prime p)] {a : ℕ} (ha₁ : n < p ^ a) (ha₂ : k < p ^ a) : ↑(n.choose k) ≡ ∏ i ∈ Finset.range a, ↑((n / p ^ i % p).choose (k / p ^ i % p)) [ZMOD ↑p]

Lucas's Theorem: For primes p, choose n k is congruent to the product of choose (⌊n / p ^ i⌋ % p) (⌊k / p ^ i⌋ % p) over i modulo p.

theorem Choose.choose_modEq_prod_range_choose_nat {n : ℕ} {k : ℕ} {p : ℕ} [Fact (Nat.Prime p)] {a : ℕ} (ha₁ : n < p ^ a) (ha₂ : k < p ^ a) : n.choose k ≡ ∏ i ∈ Finset.range a, (n / p ^ i % p).choose (k / p ^ i % p) [MOD p]

Lucas's Theorem: For primes p, choose n k is congruent to the product of choose (⌊n / p ^ i⌋ % p) (⌊k / p ^ i⌋ % p) over i modulo p.

theorem Choose.lucas_theorem {n : ℕ} {k : ℕ} {p : ℕ} [Fact (Nat.Prime p)] {a : ℕ} (ha₁ : n < p ^ a) (ha₂ : k < p ^ a) : ↑(n.choose k) ≡ ∏ i ∈ Finset.range a, ↑((n / p ^ i % p).choose (k / p ^ i % p)) [ZMOD ↑p]

Alias of Choose.choose_modEq_prod_range_choose.

---

Lucas's Theorem: For primes p, choose n k is congruent to the product of choose (⌊n / p ^ i⌋ % p) (⌊k / p ^ i⌋ % p) over i modulo p.

theorem Choose.lucas_theorem_nat {n : ℕ} {k : ℕ} {p : ℕ} [Fact (Nat.Prime p)] {a : ℕ} (ha₁ : n < p ^ a) (ha₂ : k < p ^ a) : n.choose k ≡ ∏ i ∈ Finset.range a, (n / p ^ i % p).choose (k / p ^ i % p) [MOD p]

Alias of Choose.choose_modEq_prod_range_choose_nat.

---

Lucas's Theorem: For primes p, choose n k is congruent to the product of choose (⌊n / p ^ i⌋ % p) (⌊k / p ^ i⌋ % p) over i modulo p.