Theorems · Theorem · number theory

Nat.Prime.emultiplicity_factorial_mul_succ

∀ {n p : ℕ},
  Nat.Prime p →
    emultiplicity p (p * (n + 1)).factorial = emultiplicity p (p * n).factorial + emultiplicity p (n + 1) + 1

The multiplicity of p in (p * (n + 1))! is one more than the sum of the multiplicities of p in (p * n)! and n + 1.

Defined in

Mathlib.Data.Nat.Multiplicity

Cited by

1 results in Mathlib

Foundations

Depth 78 from the axioms · uses propext, Classical.choice, Quot.sound