gcd_threehundredsixty_eighthundredforty
plain-language theorem explainer
The equality gcd(360, 840) = 120 is recorded as a verified fact in the natural numbers. Number theorists checking concrete multiples during arithmetic function work in the Recognition framework would reference it for quick numerical grounding. The proof is a one-line wrapper that delegates the entire computation to native_decide.
Claim. $ gcd(360, 840) = 120 $
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. This theorem supplies a concrete numerical identity that can anchor calculations involving multiples of 120 in the surrounding primes section. No upstream lemmas are required.
proof idea
The proof is a one-line wrapper that applies native_decide to evaluate the gcd directly.
why it matters
The identity provides a basic numerical checkpoint inside the arithmetic functions module but carries no recorded downstream uses. It supports lightweight numerical checks that may precede Möbius or squarefree arguments without invoking the forcing chain, RCL, or phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.