vp_factorial_four_two
plain-language theorem explainer
The exponent of prime 2 in the factorization of 4! equals 3. Researchers verifying explicit prime exponents for small integers cite this as a base computation. The proof is a one-line wrapper that invokes native_decide to evaluate the factorization map directly.
Claim. The exponent of the prime 2 in the prime factorization of $4!$ equals 3.
background
vp(p, n) extracts the exponent of prime p in the factorization of n, implemented directly as n.factorization p. The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function and including concrete valuation checks such as this one. Upstream the definition of vp appears in the Factorization module as a direct extraction from the prime factorization map.
proof idea
The proof is a one-line wrapper that applies the native_decide tactic to compute the equality by evaluating the factorization of 4! and reading off the exponent of 2.
why it matters
This supplies a verified base case for the valuation function on small factorials inside the primes arithmetic layer. It supports explicit computations that feed into broader factorization results, consistent with the module's role in providing Möbius footholds and direct checks before deeper Dirichlet algebra is added.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.