English
For any p prime, and nonnegative n,k with k ≤ n and k ≠ 0, the p-adic exponent of n! is at most the sum of the p-adic exponents of C(n,k) and k!
Русский
Для любого простого p и неотрицательных n,k с k ≤ n и k ≠ 0, показатель p в n! не превышает сумму показателей в C(n,k) и в k!.
LaTeX
$$$ n!.factorization p ≤ (n \\choose k).factorization p + k!.factorization p. $$$
Lean4
/-- A lower bound on the factorization of `p` in `choose n k`. -/
theorem factorization_le_factorization_choose_add {p : ℕ} :
∀ {n k : ℕ}, k ≤ n → k ≠ 0 → n.factorization p ≤ (choose n k).factorization p + k.factorization p
| n, 0, _, _ => by tauto
| 0, x + 1, _, _ => by simp
| n + 1, k + 1, hkn, hk =>
by
rw [← Pi.add_apply, ← coe_add, ← factorization_mul (ne_of_gt <| choose_pos hkn) (zero_ne_add_one k).symm]
refine
factorization_le_factorization_of_dvd_right ?_ (zero_ne_add_one n).symm
(Nat.mul_ne_zero (ne_of_gt <| choose_pos hkn) (by positivity))
rw [← succ_mul_choose_eq]
exact dvd_mul_right _ _
