Kummer’s theorem in MathComp

6.4 Kummer via digit sums

Theorem 6.6 Kummer’s theorem — digit sum form
✓
#

Uses

Rocq declarations

For prime \(p\) and \(0 {\lt} k \leq n\),

\[ (p-1) \cdot v_p\! \binom {n}{k} = s_p(k) + s_p(n-k) - s_p(n). \]

Proof. Apply Lemma 6.5 to \(n!\), \(k!\), and \((n-k)!\), then use \(v_p\binom {n}{k} = v_p(n!) - v_p(k!) - v_p((n-k)!)\).