Theorems · Theorem · number theory

padicValNat_factorial

∀ {p n b : ℕ} [hp : Fact (Nat.Prime p)], Nat.log p n < b → padicValNat p n.factorial = ∑ i ∈ Finset.Ico 1 b, n / p ^ i

Legendre's Theorem The p-adic valuation of 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.NumberTheory.Padics.PadicVal.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

Fact