Kummer’s theorem in MathComp

6.3 Legendre via digit sums

Lemma 6.5 Legendre’s formula via digit sums

For prime \(p\) and \(n {\gt} 0\),

\[ (p-1) \cdot v_p(n!) = n - s_p(n). \]

Proof. From the digit representation \(n = \sum _i d_i(n) \cdot p^i\) and Legendre’s formula \(v_p(n!) = \sum _{k \geq 1} \lfloor n/p^k \rfloor \). A telescoping argument gives the result.