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

Co-authored-by: Aaron Hill <[email protected]> Co-authored-by: Matej Penciak <[email protected]> Co-authored-by: Austin Letson <[email protected]>
leanprover-community · Feb 1, 2025 · cbcd389 · cbcd389
1 parent 388ed47
commit cbcd389
Showing 1 changed file with 32 additions and 0 deletions.
diff --git a/Mathlib/Data/Nat/Factorial/BigOperators.lean b/Mathlib/Data/Nat/Factorial/BigOperators.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kyle Miller, Pim Otte
 -/
 import Mathlib.Data.Nat.Factorial.Basic
+import Mathlib.Algebra.BigOperators.Intervals
 import Mathlib.Algebra.Order.BigOperators.Ring.Finset
 
 /-!
@@ -41,4 +42,35 @@ 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` successive non-negative integers. -/
+private lemma factorial_coe_dvd_prod_of_nonneg (k : ℕ) (n : ℤ) (hn : 0 ≤ n) :
+    (k ! : ℤ) ∣ ∏ i ∈ range k, (n + i) := by
+  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 [hx]
+
+/-- `k!` divides the product of any `k` successive integers. -/
+lemma factorial_coe_dvd_prod (k : ℕ) (n : ℤ) : (k ! : ℤ) ∣ ∏ i ∈ range k, (n + i) := by
+  by_cases hn : n < 0
+  · by_cases hnk : 0 < n + k
+    · have : ∏ i ∈ range k, (n + ↑i) = 0 := prod_eq_zero_iff.mpr <| by
+        have ⟨negn, _⟩ : ∃ (negn : ℕ), -n = ↑negn := Int.eq_ofNat_of_zero_le <| by linarith
+        exact ⟨negn, by rw [mem_range]; omega⟩
+      rw [this]
+      exact (k ! : ℤ).dvd_zero
+    · have prod_eq : ∏ x ∈ range k, |n + ↑x| =  ∏ x ∈ range k, -(n + ↑x) := by
+        refine prod_congr rfl fun _ hx ↦ ?_
+        rw [mem_range] at hx
+        rw [abs_of_neg]
+        linarith
+      rw [← dvd_abs, abs_prod, prod_eq, ← prod_range_reflect]
+      simp_rw [neg_add_rev, add_comm]
+      rw [show ∏ j ∈ range k, (-n + -↑(k - 1 - j)) = ∏ j ∈ range k, (-n + -↑(k - 1) + j) from ?_]
+      · exact factorial_coe_dvd_prod_of_nonneg k (-n + -↑(k - 1)) (by omega)
+      · refine prod_congr rfl fun _ ↦ ?_
+        rw [mem_range]
+        omega
+  · exact factorial_coe_dvd_prod_of_nonneg k n <| not_lt.mp hn
+
 end Nat