primorial_five_eq
plain-language theorem explainer
The equality primorial(5) = 2310 holds by direct computation of the product of the first five primes. Number theorists referencing arithmetic functions or small primorials in larger proofs would cite this identity for verification. The proof proceeds via a native decision procedure that confirms the numerical match without manual expansion.
Claim. $p_5 = 2310$ where $p_5$ denotes the primorial of 5, i.e., the product of the first five primes $2,3,5,7,11$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function and its basic properties such as vanishing on non-squarefree arguments. Local conventions treat primorial(n) as the product of the first n primes, here specialized to n=5. No upstream lemmas are invoked; the statement stands as an isolated numerical anchor within the arithmetic-functions file.
proof idea
The proof is a one-line wrapper that invokes the native_decide tactic to verify the integer equality by direct computation.
why it matters
This identity anchors subsequent calculations with 2310, such as the totient value phi(2310)=480 noted in the immediate module comment. It supplies a concrete numerical fact for arithmetic contexts in the Recognition framework, though no downstream theorems currently reference it and no chain steps from T0-T8 or the Recognition Composition Law are involved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.