lcm_eight_eighthundredforty
plain-language theorem explainer
The equality lcm(8, 840) = 840 holds for natural numbers. Number theorists using arithmetic functions may cite this when confirming that 840 is a multiple of 8 in divisibility checks. The proof is a direct term-mode evaluation via native decision procedure.
Claim. $lcm(8, 840) = 840$
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. Basic divisibility facts sit alongside these wrappers to support later inversion steps. The local setting keeps statements minimal before deeper Dirichlet algebra is added.
proof idea
The proof is a one-line term wrapper that applies native_decide to evaluate the lcm computation directly.
why it matters
This equality supplies a concrete arithmetic check inside the module's infrastructure for Möbius footholds. No parent theorems or downstream results are recorded. It touches no Recognition Science landmarks such as the forcing chain or phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.