factorization_factorial_mul — 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

/-- The factorization of `p` in `(p * n)!` is `n` more than that of `n!`. -/
theorem factorization_factorial_mul {n p : ℕ} (hp : p.Prime) : (p * n)!.factorization p = (n)!.factorization p + n := by
  induction n with
  | zero => simp
  | succ n
    ih =>
    simp [factorization_factorial_mul_succ hp, ih, factorial_succ,
      factorization_mul (zero_ne_add_one n).symm (factorial_ne_zero n)]
    ring

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