Kummer’s theorem in MathComp
1
Existing MathComp infrastructure
▶
1.1
Prime and p-adic valuation
1.2
Binomial coefficients and factorials
1.3
Euclidean division
2
Carry arithmetic
▶
2.1
The floor-division addition identity
2.2
The carry predicate
2.3
Summed carry-count identity
3
Connecting Legendre’s formula to binomial coefficients
▶
3.1
Extending Legendre sums
3.2
p-adic valuation of binomial coefficients
4
Kummer’s theorem
5
Corollaries for binomial factorizations
6
Digit sums and the alternative Kummer formulation
▼
6.1
Digit extraction
6.2
Digit sum
6.3
Legendre via digit sums
6.4
Kummer via digit sums
Dependency graph
6.2 Digit sum
Definition
6.4
Digit sum
✓
#
Uses
Definition 6.1
Rocq
Rocq declarations
MathCompKummer.digit_sum.digit_sum
The sum of base-\(p\) digits of \(n\):
\[ s_p(n) := \sum _{i=0}^{\texttt{trunc\_ log}(p,n)} d_i(n). \]