vp_factorial_six_two
plain-language theorem explainer
The declaration establishes that the exponent of prime 2 in the factorization of 6! equals 4. Researchers computing small factorial valuations or verifying base cases for arithmetic functions would reference it. The proof is a direct native computation that evaluates the factorial and its 2-adic exponent without manual expansion.
Claim. $v_2(6!)=4$, where $v_p(n)$ denotes the exponent of prime $p$ in the prime factorization of $n$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function and related maps such as bigOmega. The upstream definition states that vp p n is the exponent of p in the prime factorization of n, implemented directly as n.factorization p. This theorem sits among sibling results on Möbius values and squarefree detection, all kept minimal until deeper Dirichlet algebra is added.
proof idea
One-line wrapper that applies native_decide to evaluate Nat.factorial 6 and extract its factorization exponent for p=2.
why it matters
It supplies a verified numerical base case for factorial valuations inside the arithmetic-functions module. The module documentation frames these as footholds for Möbius inversion once interfaces stabilize; the result aligns with that incremental strategy even though no downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.