English
Let p be a prime. For all nonnegative integers n and k, the binomial coefficient satisfies C(n,k) ≡ C(n mod p, k mod p) · C(n/p, k/p) (mod p).
Русский
Пусть p — простое число. Для любых неотрицательных n, k выполняется C(n, k) ≡ C(n mod p, k mod p) · C(n/p, k/p) (mod p).
LaTeX
$$$ \\binom{n}{k} \\equiv \\binom{n \\bmod p}{k \\bmod p} \\cdot \\binom{n / p}{k / p} \\pmod p. $$$
Lean4
/-- 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_modEq_choose_mod_mul_choose_div :
choose n k ≡ choose (n % p) (k % p) * choose (n / p) (k / p) [ZMOD p] :=
by
have decompose : ((X : (ZMod p)[X]) + 1) ^ n = (X + 1) ^ (n % p) * (X ^ p + 1) ^ (n / p) := by
simpa using add_pow_eq_mul_pow_add_pow_div_char (X : (ZMod p)[X]) 1 p _
simp only [← ZMod.intCast_eq_intCast_iff, ← coeff_X_add_one_pow _ n k, ← eq_intCast (Int.castRingHom (ZMod p)),
← coeff_map, Polynomial.map_pow, Polynomial.map_add, Polynomial.map_one, map_X, decompose]
simp only [add_pow, one_pow, mul_one, ← pow_mul, sum_mul_sum]
conv_lhs =>
enter [1, 2, k, 2, k']
rw [← mul_assoc, mul_right_comm _ _ (X ^ (p * k')), ← pow_add, mul_assoc, ← cast_mul]
have h_iff : ∀ x ∈ range (n % p + 1) ×ˢ range (n / p + 1), k = x.1 + p * x.2 ↔ (k % p, k / p) = x :=
by
intro ⟨x₁, x₂⟩ hx
rw [Prod.mk.injEq]
constructor <;> intro h
· simp only [mem_product, mem_range] at hx
have h' : x₁ < p := lt_of_lt_of_le hx.left <| mod_lt _ Fin.pos'
rw [h, add_mul_mod_self_left, add_mul_div_left _ _ Fin.pos', eq_comm (b := x₂)]
exact ⟨mod_eq_of_lt h', right_eq_add.mpr (div_eq_of_lt h')⟩
· rw [← h.left, ← h.right, mod_add_div]
simp only [finset_sum_coeff, coeff_mul_natCast, coeff_X_pow, ite_mul, zero_mul, ← cast_mul]
rw [← sum_product', sum_congr rfl (fun a ha ↦ if_congr (h_iff a ha) rfl rfl), sum_ite_eq]
split_ifs with h
· simp
· rw [mem_product, mem_range, mem_range, not_and_or, lt_succ, not_le, not_lt] at h
cases h <;> simp [choose_eq_zero_of_lt (by tauto)]
