Theorems · Theorem · number theory

Nat.Prime.multiplicity_factorial_pow

∀ {n p : ℕ}, Nat.Prime p → multiplicity p (p ^ n).factorial = ∑ i ∈ Finset.range n, p ^ i

The multiplicity of a prime p in p ^ n is the sum of p ^ i, where i ranges between 0 and n - 1.

Defined in

Mathlib.Data.Nat.Multiplicity

Cited by

0 results in Mathlib

Foundations

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