factorization_choose_le_one — Mathlib

English

For all n,k with k ≤ n, the p-adic exponent in n! is at most the sum of the p-adic exponent in (n choose k) and in k!, i.e., n!_p ≤ (n choose k)!_p + k!_p.

Русский

Для всех n,k с k ≤ n показатель p в n! не превосходит сумму показателей в (n choose k) и в k!, т.е. n!_p ≤ (n choose k)!_p + k!_p.

LaTeX

$$$ n!.factorization p ≤ (n \\choose k).factorization p + k!.factorization p. $$$

Lean4

/-- Primes greater than about `sqrt n` appear only to multiplicity 0 or 1
in the binomial coefficient. -/
theorem factorization_choose_le_one (p_large : n < p ^ 2) : (choose n k).factorization p ≤ 1 :=
  by
  apply factorization_choose_le_log.trans
  rcases eq_or_ne n 0 with (rfl | hn0); · simp
  exact Nat.lt_succ_iff.1 (log_lt_of_lt_pow hn0 p_large)

Похожие утверждения