twohundredten_eq_primorial_four
plain-language theorem explainer
The equality 210 equals the product of the first four primes holds in the natural numbers. Researchers evaluating arithmetic functions such as the Möbius function or Euler's totient at small composites would cite this identity. The proof is a direct computational verification via Lean's native decision procedure.
Claim. The natural number 210 equals the product of the first four primes: $210 = 2 × 3 × 5 × 7$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. This theorem supplies a concrete numerical identity for evaluating such functions at the composite 210. The local setting consists of small footholds for Dirichlet algebra and inversion once basic interfaces stabilize.
proof idea
The proof is a one-line term that applies native_decide to confirm the numerical equality by direct computation.
why it matters
This identity anchors small-case computations in the arithmetic functions module. It supports evaluations such as the totient at 210, noted in the accompanying comment. It fills a concrete numerical step in the NumberTheory.Primes development without depending on upstream lemmas from the forcing chain or Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.