vp_factorial_fifty_seven
plain-language theorem explainer
The theorem asserts that the exponent of prime 7 in the prime factorization of 50! equals 8. Number theorists computing explicit valuations for factorials or binomial coefficients would cite this concrete result. The proof is a direct computational verification that applies native_decide to the factorization map.
Claim. $v_7(50!) = 8$, where $v_p(n)$ denotes the exponent of prime $p$ in the prime factorization of the natural number $n$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function. The function vp extracts the exponent of a given prime from the factorization of its argument, as defined by vp p n := n.factorization p. This declaration evaluates the case p = 7 and n = 50!.
proof idea
The proof is a one-line wrapper that applies native_decide to reduce the equality to a decidable computation of the prime factorization of 50! and the multiplicity of the factor 7.
why it matters
It supplies a verified numerical anchor inside the arithmetic-functions file. No immediate parent theorems are recorded among the used-by edges, yet the value supports explicit calculations that may feed later arguments involving prime powers. The surrounding module context emphasizes Möbius and squarefree properties, with this instance providing supporting concrete data.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.