gcd_eight_eighthundredforty
plain-language theorem explainer
The equality gcd(8, 840) = 8 holds for natural numbers. Number theorists working with arithmetic functions over multiples of small primes would cite this basic divisibility relation. The proof is a one-line wrapper that invokes native_decide to evaluate the gcd directly.
Claim. $ gcd(8, 840) = 8 $
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. This theorem records a concrete divisibility fact between 8 and 840 with no additional hypotheses. No upstream results are invoked; the statement is self-contained within the NumberTheory.Primes.ArithmeticFunctions setting.
proof idea
The proof is a one-line wrapper that applies native_decide to compute the gcd value directly.
why it matters
This equality supplies a verified computational anchor for divisibility checks involving 840 in prime arithmetic contexts. It fills a basic gap in the module without depending on or feeding into other declarations in the current graph.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.