Documentation

Mathlib.Data.Nat.Choose.Lucas

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 #

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)) * (∏ iFinset.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) iFinset.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 iFinset.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) iFinset.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 iFinset.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.