gcd_fortyfive_eighthundredforty
plain-language theorem explainer
The greatest common divisor of 45 and 840 equals 15. Number theorists working with arithmetic functions might cite this for quick divisor checks in prime-related work. The proof relies on a single native decision procedure that evaluates the expression directly.
Claim. $gcd(45, 840) = 15$
background
This declaration appears in the module on arithmetic functions that supplies lightweight wrappers around Mathlib's library, starting with the Möbius function. The local theoretical setting emphasizes basic interfaces before layering deeper Dirichlet algebra and inversion. No upstream lemmas are invoked.
proof idea
The proof is a one-line wrapper applying the native_decide tactic to compute and verify the gcd.
why it matters
This supplies a concrete numerical fact within the primes arithmetic functions section. It supports the sibling results on the Möbius function such as mobius_prime. No connection to the main Recognition Science landmarks like the eight-tick octave or D=3 is present.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.