Lucas' theorem with a nonzero last digit on top

Mathlib's Choose.choose_mul_mul_modEq_choose_nat reduces choose (p * a) (p * b) modulo a prime p to choose a b. This file records the companion case in which the upper index has a nonzero last base-p digit c < p and the lower index is still divisible by p: the extra digit contributes the factor choose c 0 = 1. At p = 2 it computes the parity of choose (2a + 1) (2b), which is what sign bookkeeping with binomial exponents of odd upper index needs.

Main results

• Choose.choose_mul_add_mul_modEq_choose_nat: choose (p * a + c) (p * b) ≡ choose a b [MOD p] for c < p.

theorem Choose.choose_mul_add_mul_modEq_choose_nat {p a b c : ℕ} [Fact (Nat.Prime p)] (hc : c < p) : (p * a + c).choose (p * b) ≡ a.choose b [MOD p]

For primes p and c < p, choose (p * a + c) (p * b) is congruent to choose a b modulo p. This is Lucas' theorem for a lower index divisible by p.