vp_factorial_twentyfive_five
plain-language theorem explainer
The exponent of the prime 5 in the prime factorization of 25! equals 6. Number theorists verifying explicit valuations in factorials cite this result for direct checks. The proof evaluates the definition of the valuation function directly via native decision procedures.
Claim. The 5-adic valuation satisfies $v_5(25!) = 6$.
background
The function vp p n extracts the exponent of prime p in the factorization of n, implemented directly as n.factorization p. This theorem sits in a module supplying lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function and related squarefree checks. The upstream definition of vp supplies the sole dependency, allowing the statement to reduce to a concrete computation on Nat.factorial.
proof idea
One-line wrapper that applies native_decide to evaluate the factorization exponent.
why it matters
The result supplies an explicit numerical check inside the arithmetic functions module. It supports downstream verification of prime-power counts in factorials, consistent with the module's focus on Möbius footholds and basic Dirichlet tools. No open questions or scaffolding are attached.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.