primorial_two_eq
plain-language theorem explainer
Primorial of two equals six as the product of the first two primes. Number theorists building inductive arguments on prime products would cite this base case. The proof reduces to a single native decision procedure that verifies the arithmetic identity directly.
Claim. The primorial of 2 equals 6, that is, the product of the first two primes satisfies $2 × 3 = 6$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function. Primorial(n) denotes the product of the first n primes. This theorem fixes the n=2 case with no upstream lemmas required.
proof idea
The proof is a one-line term wrapper that applies the native_decide tactic to confirm the numerical equality on natural numbers.
why it matters
This base equality anchors primorial computations before Möbius-related properties are developed in the same module. It supplies the initial concrete value in the arithmetic functions library. No open questions or downstream applications are recorded.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.