pow_factorization_choose_le — Mathlib

English

For a prime p, the p-adic exponent of (p·n)! equals the p-adic exponent of n! plus n.

Русский

Для простого p показатель p в (p·n)! равен показателю p в n! плюс n.

LaTeX

$$$ (p \\cdot n)!.factorization p = (n)!.factorization p + n. $$$

Lean4

/-- A `pow` form of `Nat.factorization_choose_le` -/
theorem pow_factorization_choose_le (hn : 0 < n) : p ^ (choose n k).factorization p ≤ n :=
  pow_le_of_le_log hn.ne' factorization_choose_le_log

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