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 Digit sums and the alternative Kummer formulation