feat(Factorial): k! divides the product of any k successive integers (#…

…21332) Co-authored-by: Aaron Hill <[email protected]> Co-authored-by: Matej Penciak <[email protected]> Co-authored-by: Austin Letson <[email protected]>
leanprover-community · Feb 7, 2025 · 9bc6a09 · 9bc6a09
1 parent 12e86c1
commit 9bc6a09
Showing 1 changed file with 11 additions and 0 deletions.
diff --git a/Mathlib/Data/Nat/Factorial/BigOperators.lean b/Mathlib/Data/Nat/Factorial/BigOperators.lean
@@ -5,6 +5,7 @@ Authors: Kyle Miller, Pim Otte
 -/
 import Mathlib.Data.Nat.Factorial.Basic
 import Mathlib.Algebra.Order.BigOperators.Ring.Finset
+import Mathlib.Tactic.Zify
 
 /-!
 # Factorial with big operators
@@ -41,4 +42,14 @@ theorem descFactorial_eq_prod_range (n : ℕ) : ∀ k, n.descFactorial k = ∏ i
   | 0 => rfl
   | k + 1 => by rw [descFactorial, prod_range_succ, mul_comm, descFactorial_eq_prod_range n k]
 
+/-- `k!` divides the product of any `k` consecutive integers. -/
+lemma factorial_coe_dvd_prod (k : ℕ) (n : ℤ) : (k ! : ℤ) ∣ ∏ i ∈ range k, (n + i) := by
+  rw [Int.dvd_iff_emod_eq_zero, Finset.prod_int_mod]
+  simp_rw [← Int.emod_add_emod n]
+  have hn : 0 ≤ n % k ! := Int.emod_nonneg n <| Int.natCast_ne_zero.mpr k.factorial_ne_zero
+  obtain ⟨x, hx⟩ := Int.eq_ofNat_of_zero_le hn
+  have hdivk := x.factorial_dvd_ascFactorial k
+  zify [x.ascFactorial_eq_prod_range k] at hdivk
+  rwa [← Finset.prod_int_mod, ← Int.dvd_iff_emod_eq_zero, hx]
+
 end Nat