primorial_four_eq
plain-language theorem explainer
The equality primorial of 4 equals 210 holds by direct computation of the product of the first four primes. Number theorists working with arithmetic functions or prime products would reference this for quick verification in larger proofs. The proof is a single native decision tactic that evaluates the equality in the natural numbers.
Claim. The fourth primorial equals the product of the first four primes: $210 = 2 × 3 × 5 × 7$.
background
This declaration appears in the module supplying lightweight wrappers around Mathlib's arithmetic function library, beginning with the Möbius function μ. The local theoretical setting keeps statements minimal so that deeper Dirichlet algebra and inversion can be added once basic interfaces stabilize. Primorial denotes the product of the first n primes; the present case fixes n = 4 and records the resulting integer value.
proof idea
The proof is a one-line term that applies native_decide to evaluate the concrete equality between 210 and the expanded product in the naturals.
why it matters
This concrete equality anchors primorial calculations inside the NumberTheory.Primes component of the Recognition Science formalization. It supplies a verified base case for arithmetic-function work that may later feed into prime-counting or inversion arguments, even though no immediate parent theorems or downstream uses are recorded. In the wider framework it contributes to the number-theoretic scaffolding that supports the forcing chain from T0 through T8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.