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.

theorem Choose.choose_mul_mul_modEq_choose {a b p : ℕ} [Fact (Nat.Prime p)] : ↑((p * a).choose (p * b)) ≡ ↑(a.choose b) [ZMOD ↑p]

For primes p, choose (p * a) (p * b) is congruent to choose a b modulo p. Also see choose_mul_mul_modEq_choose_nat for the version with MOD.

theorem Choose.choose_mul_mul_modEq_choose_nat {a b p : ℕ} [Fact (Nat.Prime p)] : (p * a).choose (p * b) ≡ a.choose b [MOD p]

For primes p, choose (p * a) (p * b) is congruent to choose a b modulo p. Also see choose_mul_mul_modEq_choose for the version with ZMOD.

theorem Choose.choose_pow_mul_pow_mul_modEq_choose {k a b p : ℕ} [Fact (Nat.Prime p)] : ↑((p ^ k * a).choose (p ^ k * b)) ≡ ↑(a.choose b) [ZMOD ↑p]

For primes p, choose (p ^ k * a) (p ^ k * b) is congruent to choose a b modulo p. Also see choose_pow_mul_pow_mul_modEq_choose_nat for the version with MOD.

theorem Choose.choose_pow_mul_pow_mul_modEq_choose_nat {k a b p : ℕ} [Fact (Nat.Prime p)] : (p ^ k * a).choose (p ^ k * b) ≡ a.choose b [MOD p]

For primes p, choose (p ^ k * a) (p ^ k * b) is congruent to choose a b modulo p. Also see choose_pow_mul_pow_mul_modEq_choose for the version with ZMOD.

theorem Choose.eq_pow_multiplicity_of_choose_modEq_zero {n p : ℕ} [Fact (Nat.Prime p)] (hn : 0 < n) (h : ∀ i ∈ Finset.Icc 1 (n - 1), ↑(n.choose i) ≡ 0 [ZMOD ↑p]) : n = p ^ multiplicity p n

For primes p and positive integer n, assume that for all i ∈ Icc 1 (n - 1), choose n i congruent to 0 module p, then n = p ^ multiplicity p n. Also see eq_pow_multiplicity_of_choose_modEq_zero_nat for the version with MOD.

theorem Choose.eq_pow_multiplicity_of_choose_modEq_zero_nat {n p : ℕ} [Fact (Nat.Prime p)] (hn : 0 < n) (h : ∀ i ∈ Finset.Icc 1 (n - 1), n.choose i ≡ 0 [MOD p]) : n = p ^ multiplicity p n

For primes p and positive integer n, assume that for all i ∈ Icc 1 (n - 1), choose n i congruent to 0 module p, then n = p ^ multiplicity p n. Also see eq_pow_multiplicity_of_choose_modEq_zero for the version with ZMOD.

theorem Choose.minFac_dvd_gcd_choose_of_isPrimePow {n : ℕ} (h : IsPrimePow n) : n.minFac ∣ (Finset.Icc 1 (n - 1)).gcd n.choose

For a prime power n, the minimal prime factor divides the greatest common divisor of choose n 1, ⋯, choose n (n - 1).

theorem Choose.minFac_sq_ndvd_gcd_choose_of_isPrimePow {n : ℕ} (h : IsPrimePow n) : ¬n.minFac ^ 2 ∣ (Finset.Icc 1 (n - 1)).gcd n.choose

theorem Choose.primeFactors_gcd_choose_of_isPrimePow {n : ℕ} (h : IsPrimePow n) : ((Finset.Icc 1 (n - 1)).gcd n.choose).primeFactors = {n.minFac}

theorem Choose.gcd_choose_eq_minFac_of_isPrimePow {n : ℕ} (h : IsPrimePow n) : (Finset.Icc 1 (n - 1)).gcd n.choose = n.minFac

For a prime power n, the greatest common divisor of choose n 1, ⋯, choose n (n - 1) is actually the minimal prime factor of n.

theorem Choose.gcd_choose_eq_one_of_not_isPrimePow {n : ℕ} (hn : 1 < n) (hpn : ¬IsPrimePow n) : (Finset.Icc 1 (n - 1)).gcd n.choose = 1

For a natural number n greater than 1, assume that n is not a prime power, then the greatest common divisor of choose n 1, ⋯, choose n (n - 1) is 1.