feat(Data/Nat/Choose): Lucas' theorem

Mathlib.lean

@@ -2264,6 +2264,7 @@ import Mathlib.Data.Nat.Choose.Cast
 import Mathlib.Data.Nat.Choose.Central
 import Mathlib.Data.Nat.Choose.Dvd
 import Mathlib.Data.Nat.Choose.Factorization
+import Mathlib.Data.Nat.Choose.Lucas
 import Mathlib.Data.Nat.Choose.Multinomial
 import Mathlib.Data.Nat.Choose.Sum
 import Mathlib.Data.Nat.Choose.Vandermonde

Mathlib/Algebra/CharP/Basic.lean

@@ -110,6 +110,11 @@ theorem add_pow_char_pow [CommSemiring R] {p : ℕ} [Fact p.Prime] [CharP R p] {
     (x + y) ^ p ^ n = x ^ p ^ n + y ^ p ^ n :=
   add_pow_char_pow_of_commute _ _ _ (Commute.all _ _)
 
+theorem add_pow_eq_add_pow_mod_mul_pow_add_pow_div
+    [CommSemiring R] {p : ℕ} [Fact p.Prime] [CharP R p] {n : ℕ} (x y : R) :
+    (x + y) ^ n = (x + y) ^ (n % p) * (x ^ p + y ^ p) ^ (n / p) := by
+  rw [← add_pow_char, ← pow_mul, ← pow_add, Nat.mod_add_div]
+
 theorem sub_pow_char [CommRing R] {p : ℕ} [Fact p.Prime] [CharP R p] (x y : R) :
     (x - y) ^ p = x ^ p - y ^ p :=
   sub_pow_char_of_commute _ _ _ (Commute.all _ _)
@@ -118,6 +123,11 @@ theorem sub_pow_char_pow [CommRing R] {p : ℕ} [Fact p.Prime] [CharP R p] {n :
     (x - y) ^ p ^ n = x ^ p ^ n - y ^ p ^ n :=
   sub_pow_char_pow_of_commute _ _ _ (Commute.all _ _)
 
+theorem sub_pow_eq_sub_pow_mod_mul_pow_sub_pow_div
+    [CommRing R] {p : ℕ} [Fact p.Prime] [CharP R p] {n : ℕ} (x y : R) :
+    (x - y) ^ n = (x - y) ^ (n % p) * (x ^ p - y ^ p) ^ (n / p) := by
+  rw [← sub_pow_char, ← pow_mul, ← pow_add, Nat.mod_add_div]
+
 theorem CharP.neg_one_pow_char [Ring R] (p : ℕ) [CharP R p] [Fact p.Prime] :
     (-1 : R) ^ p = -1 := by
   rw [eq_neg_iff_add_eq_zero]

Mathlib/Data/Nat/Choose/Lucas.lean

@@ -0,0 +1,100 @@
+/-
+Copyright (c) 2023 Gareth Ma. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Gareth Ma
+-/
+import Mathlib.Data.ZMod.Basic
+import Mathlib.RingTheory.Polynomial.Basic
+
+/-!
+# Lucas's theorem
+
+This file contains a proof of [Lucas's theorem](https://en.wikipedia.org/wiki/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.
+-/
+
+open Finset hiding choose
+
+open Nat BigOperators Polynomial
+
+namespace Choose
+
+variable {n k p : ℕ} [Fact p.Prime]
+
+/-- 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_add_pow_mod_mul_pow_add_pow_div _ (X : (ZMod p)[X]) 1
+  simp only [← ZMod.intCast_eq_intCast_iff, Int.cast_mul, Int.cast_ofNat,
+    ← 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.size_pos'
+      rw [h, add_mul_mod_self_left, add_mul_div_left _ _ Fin.size_pos', eq_comm (b := x₂)]
+      exact ⟨mod_eq_of_lt h', self_eq_add_left.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)]
+
+/-- 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_modEq_choose_mod_mul_choose_div_nat :
+    choose n k ≡ choose (n % p) (k % p) * choose (n / p) (k / p) [MOD p] := by
+  rw [← Int.natCast_modEq_iff]
+  exact_mod_cast choose_modEq_choose_mod_mul_choose_div
+
+/-- 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_modEq_choose_mul_prod_range_choose (a : ℕ) :
+    choose n k ≡ choose (n / p ^ a) (k / p ^ a) *
+      ∏ i in range a, choose (n / p ^ i % p) (k / p ^ i % p) [ZMOD p] :=
+  match a with
+  | Nat.zero => by simp
+  | Nat.succ a => (choose_modEq_choose_mul_prod_range_choose a).trans <| by
+    rw [prod_range_succ, cast_mul, ← mul_assoc, mul_right_comm]
+    gcongr
+    apply choose_modEq_choose_mod_mul_choose_div.trans
+    simp_rw [pow_succ, Nat.div_div_eq_div_mul, mul_comm]
+    rfl
+
+/-- **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_modEq_prod_range_choose {a : ℕ} (ha₁ : n < p ^ a) (ha₂ : k < p ^ a) :
+    choose n k ≡ ∏ i in range a, choose (n / p ^ i % p) (k / p ^ i % p) [ZMOD p] := by
+  apply (choose_modEq_choose_mul_prod_range_choose a).trans
+  simp_rw [Nat.div_eq_of_lt ha₁, Nat.div_eq_of_lt ha₂, choose, cast_one, one_mul, cast_prod,
+    Int.ModEq.refl]
+
+/-- **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_modEq_prod_range_choose_nat {a : ℕ} (ha₁ : n < p ^ a) (ha₂ : k < p ^ a) :
+    choose n k ≡ ∏ i in range a, choose (n / p ^ i % p) (k / p ^ i % p) [MOD p] := by
+  rw [← Int.natCast_modEq_iff]
+  exact_mod_cast choose_modEq_prod_range_choose ha₁ ha₂
+
+alias lucas_theorem := choose_modEq_prod_range_choose
+alias lucas_theorem_nat := choose_modEq_prod_range_choose_nat
+
+end Choose