vp_factorial_ten_three
plain-language theorem explainer
The exponent of the prime 3 in the prime factorization of 10! equals 4. Number theorists computing exact powers of small primes inside factorials for combinatorial counts or arithmetic-function identities would cite this result. The proof is a direct native evaluation of the factorization map.
Claim. The 3-adic valuation of $10!$ equals 4.
background
The function vp p n extracts the exponent of prime p in the factorization of natural number n. This module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function and related square-free tests. The upstream definition states that vp p n is exactly n.factorization p, which isolates the precise power of p dividing n.
proof idea
One-line wrapper that applies native_decide to evaluate the factorization exponent directly.
why it matters
This supplies a verified numerical fact for the 3-adic valuation of 10!, supporting downstream calculations in prime factorization and arithmetic functions within the Recognition Science number theory layer. It fills a concrete instance in the arithmetic functions module, though no immediate parent theorem depends on it yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.