primorial_three_eq
plain-language theorem explainer
The equality asserts that the primorial of three equals thirty, where primorial denotes the product of the first three primes. Number theorists working with small cases in arithmetic functions or sieve methods would cite this identity to anchor base computations. The proof reduces to a single native_decide tactic that evaluates the product directly.
Claim. The product of the first three primes equals thirty: $2 × 3 × 5 = 30$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. Primorial here is the product of successive primes, with this declaration fixing the value at the third prime. No upstream lemmas appear in the dependency graph, so the result stands on direct evaluation.
proof idea
The proof is a one-line wrapper that applies the native_decide tactic to compute the arithmetic expression 2 * 3 * 5 and confirm equality with 30.
why it matters
This supplies a verified base case for primorial values inside the arithmetic-functions layer. It supports later statements on Möbius inversion and square-free detection by fixing the small-prime product explicitly. No downstream uses are recorded yet, and the declaration touches none of the T0-T8 forcing chain or Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.