From 8c7a6879291233f82072dcc7d6930f06162c972f Mon Sep 17 00:00:00 2001 From: Julian Berman Date: Wed, 5 Feb 2025 00:24:45 +0000 Subject: [PATCH] feat(Factorial): k! divides the product of any k successive integers (#21332) Co-authored-by: Aaron Hill Co-authored-by: Matej Penciak Co-authored-by: Austin Letson --- Mathlib/Data/Nat/Factorial/BigOperators.lean | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/Mathlib/Data/Nat/Factorial/BigOperators.lean b/Mathlib/Data/Nat/Factorial/BigOperators.lean index 606f5b7c49b2d..45b4068aa1eea 100644 --- 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