emultiplicity_factorial_mul — Mathlib

English

For a prime p, ν_p((p n)!) = ν_p(n!) + n.

Русский

Для простого p: ν_p((p n)!) = ν_p(n!) + n.

LaTeX

$$$ emultiplicity(p, (p \cdot n)!) = emultiplicity(p, n!) + n $$$

Lean4

/-- The multiplicity of `p` in `(p * n)!` is `n` more than that of `n!`. -/
theorem emultiplicity_factorial_mul {n p : ℕ} (hp : p.Prime) : emultiplicity p (p * n)! = emultiplicity p n ! + n := by
  induction n with
  | zero => simp
  | succ n
    ih =>
    simp only [hp, emultiplicity_factorial_mul_succ, ih, factorial_succ, emultiplicity_mul, cast_add, cast_one,
      ← add_assoc]
    congr 1
    rw [add_comm, add_assoc]
      /- The multiplicity of a prime `p` in `p ^ n` is the sum of `p ^ i`, where `i` ranges between `0`
        and `n - 1`. -/

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