vp_factorial_nine_three
plain-language theorem explainer
The theorem states that the exponent of 3 in the prime factorization of 9! equals 4. Number theorists needing explicit small-factorial valuations for arithmetic computations would cite it. The proof is a one-line wrapper that invokes native_decide to evaluate the factorization directly.
Claim. Let $v_p(n)$ denote the exponent of prime $p$ in the factorization of natural number $n$. Then $v_3(9!) = 4$.
background
The function vp p n returns the exponent of prime p in the factorization of n, implemented as n.factorization p. This result appears in the module on arithmetic functions that supplies lightweight wrappers around Mathlib's library, beginning with the Möbius function for later inversion formulas. It rests on the upstream vp definition from the Factorization module.
proof idea
The proof is a one-line wrapper that applies native_decide to compute the factorization of 9! and read off the coefficient of 3.
why it matters
This supplies a concrete numerical anchor inside the arithmetic-functions development, enabling explicit checks when building toward Dirichlet algebra. It fills a small verified fact in the primes layer without touching the Recognition forcing chain, phi-ladder, or physical constants. No downstream theorems currently depend on it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.