Theorems · Theorem · number theory

Nat.Prime.emultiplicity_factorial

∀ {p : ℕ}, Nat.Prime p → ∀ {n b : ℕ}, Nat.log p n < b → emultiplicity p n.factorial = ↑(∑ i ∈ Finset.Ico 1 b, n / p ^ i)

Legendre's Theorem The multiplicity of a prime in n! is the sum of the quotients n / p ^ i. This sum is expressed over the finset Ico 1 b where b is any bound greater than log p n.

Defined in

Mathlib.Data.Nat.Multiplicity

Cited by

5 results in Mathlib

Foundations

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