factorization_factorial_le_div_pred

English

For any p prime and all n, k with k ≤ n and k ≠ 0, the p-adic exponent in n! is at most the sum of the exponent in (n choose k) and in k!

Русский

Для любого простого p и любых n,k с k ≤ n и k ≠ 0, показатель p в n! не более суммы показателя в (n choose k) и в k!.

LaTeX

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

Lean4

theorem factorization_factorial_le_div_pred {p : ℕ} (hp : p.Prime) (n : ℕ) : (n)!.factorization p ≤ (n / (p - 1) : ℕ) :=
  by
  rw [factorization_factorial hp (Nat.lt_add_one (log p n))]
  exact Nat.geom_sum_Ico_le hp.two_le _ _

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