Binomial coefficients prime to p and base-p digits

Let p be a prime. Lucas' theorem (Choose.choose_modEq_choose_mod_mul_choose_div_nat) computes n choose k modulo p digit by digit. This file draws two counting consequences.

• The number of k ≤ n with p ∤ n choose k is ∏ⱼ (nⱼ + 1), where the nⱼ are the base-p digits of n: such k are exactly those whose every digit satisfies kⱼ ≤ nⱼ.
• Every n choose k with k ≤ n is prime to p exactly when n + 1 = (a + 1) pᵐ for some a < p and some m, that is, when every base-p digit of n except the leading one is p - 1.

Both are proved by peeling off the last digit, writing n = r + p q with r < p, from the one-digit divisibility criterion Nat.dvd_choose_add_mul_iff.

These are the numerical inputs to the representation theory of SL₂ in characteristic p: the simple module of highest weight n has dimension ∏ⱼ (nⱼ + 1), and the binary forms of degree n are simple exactly when n + 1 = (a + 1) pᵐ.

Main results

• Nat.dvd_choose_add_mul_iff: for r, a < p, p ∣ (r + p q) choose (a + p b) exactly when r < a or p ∣ q choose b.
• Nat.card_filter_not_dvd_choose: the number of k ≤ n with p ∤ n choose k is the product of the base-p digits of n, each increased by one.
• Nat.forall_not_dvd_choose_iff: every n choose k with k ≤ n is prime to p exactly when n + 1 = (a + 1) pᵐ with a < p.

References

• N. J. Fine, Binomial coefficients modulo a prime, Amer. Math. Monthly 54 (1947), 589–592.
• J. C. Jantzen, Representations of Algebraic Groups, 2nd ed., Part II, Chapter 3.

theorem Nat.dvd_choose_add_mul_iff {p : ℕ} [hp : Fact (Prime p)] {q r a b : ℕ} (hr : r < p) (ha : a < p) : p ∣ (r + p * q).choose (a + p * b) ↔ r < a ∨ p ∣ q.choose b

Lucas' theorem for divisibility, one digit at a time. For last digits r, a < p, the prime p divides (r + p q) choose (a + p b) exactly when r < a or p divides q choose b.

theorem Nat.card_filter_not_dvd_choose_add_mul {p : ℕ} [hp : Fact (Prime p)] {q r : ℕ} (hr : r < p) : {k ∈ Finset.range (r + p * q + 1) | ¬p ∣ (r + p * q).choose k}.card = (r + 1) * {k ∈ Finset.range (q + 1) | ¬p ∣ q.choose k}.card

The count of binomial coefficients prime to p is multiplicative in the digits. For a last digit r < p, the number of k ≤ r + p q with p ∤ (r + p q) choose k is r + 1 times the number of k ≤ q with p ∤ q choose k.

theorem Nat.card_filter_not_dvd_choose {p : ℕ} [hp : Fact (Prime p)] (n : ℕ) : {k ∈ Finset.range (n + 1) | ¬p ∣ n.choose k}.card = (List.map (fun (x : ℕ) => x + 1) (p.digits n)).prod

Fine's theorem. The number of k ≤ n for which p ∤ n choose k is ∏ⱼ (nⱼ + 1), the product over the base-p digits nⱼ of n.

theorem Nat.forall_not_dvd_choose_add_mul_iff {p : ℕ} [hp : Fact (Prime p)] {q r : ℕ} (hr : r < p) : (∀ k ≤ r + p * q, ¬p ∣ (r + p * q).choose k) ↔ (q = 0 ∨ r + 1 = p) ∧ ∀ k ≤ q, ¬p ∣ q.choose k

The binomial coefficients (r + p q) choose k, k ≤ r + p q, with last digit r < p, are all prime to p exactly when those of q are and, unless q = 0, the last digit is r = p - 1.

theorem Nat.forall_not_dvd_choose_iff {p : ℕ} [hp : Fact (Prime p)] (n : ℕ) : (∀ k ≤ n, ¬p ∣ n.choose k) ↔ ∃ a < p, ∃ (m : ℕ), n + 1 = (a + 1) * p ^ m

All binomial coefficients n choose k are prime to p exactly when n + 1 = (a + 1) pᵐ for some a < p and some m, that is, when every base-p digit of n except the leading one is p - 1.