vp_factorial_ten_two
plain-language theorem explainer
The exponent of prime 2 in the factorization of 10! equals 8. Number theorists checking small factorial valuations or arithmetic function tables cite this for direct verification. The proof is a one-line native decision that evaluates the factorization map on 10!.
Claim. $v_2(10!) = 8$
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function. The function vp extracts the exponent of a given prime in the factorization of a natural number, implemented directly as the factorization map. This result confirms the exponent of 2 specifically in 10!.
proof idea
The proof is a one-line native decision that computes the factorization of 10! and extracts the exponent of 2.
why it matters
This theorem supplies a verified instance in the arithmetic functions section of the number theory module. It supports basic checks on prime exponents in factorials within the Recognition Science scaffolding, though it carries no downstream uses and no direct link to the forcing chain or constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.