English
For any natural k and integer n, the integer k! divides the product ∏_{i=0}^{k-1} (n+i).
Русский
Для любого k и целого n: k! делит произведение ∏_{i=0}^{k-1} (n+i).
LaTeX
$$∏_{i=0}^{k-1} (n+i) \\text{ is divisible by } k! \\text{ in } \\mathbb{Z}$$
Lean4
/-- `k!` divides the product of any `k` consecutive integers. -/
theorem 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]
