vp_factorial_eight_two
plain-language theorem explainer
The exponent of the prime 2 in the prime factorization of 8! equals 7. Number theorists verifying explicit arithmetic function values for small factorials would cite this base case. The proof is a one-line native decision that evaluates the factorization directly.
Claim. $v_2(8!) = 7$.
background
The function vp(p, n) returns the exponent of prime p in the factorization of n. This module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function, to support prime-related computations. The upstream definition states that vp(p, n) is implemented as n.factorization p, giving the direct multiplicity count.
proof idea
The proof is a one-line wrapper that applies native_decide to compute the factorization exponent of 2 in 8! directly.
why it matters
This supplies a concrete base case for arithmetic function verifications in the primes module. It supports explicit checks involving factorials and valuations, though no immediate dependents appear. It aligns with the framework's reliance on small explicit number-theoretic facts to anchor higher structures such as the Möbius function.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.