vp_factorial_twelve_two
plain-language theorem explainer
The exponent of the prime 2 in the prime factorization of 12! equals 10. Number theorists verifying explicit small-integer valuations or testing arithmetic-function implementations would reference this equality. The proof is a direct computational evaluation that applies native_decide to the factorization map.
Claim. $v_2(12!) = 10$
background
The function vp p n returns the exponent of prime p in the factorization of natural number n, implemented directly as n.factorization p. This module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function, to support later Dirichlet inversion once the basic interfaces stabilize. The upstream definition vp supplies the core extraction of these exponents from the factorization.
proof idea
The proof is a one-line wrapper that invokes native_decide to evaluate the factorization of 12! at the prime 2.
why it matters
This supplies a concrete verified value for the 2-exponent in 12!, serving as an explicit test point inside the arithmetic-functions module. It anchors small-integer data for Möbius-related constructions without depending on further hypotheses. No downstream theorems currently cite it, leaving its role open for future prime-power computations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.