gcd_eight_fortyfive
plain-language theorem explainer
The declaration records that the greatest common divisor of 8 and 45 equals 1. Arithmetic function specialists working with Möbius inversions in the Recognition Science project cite it for visibility when checking squarefree conditions or handling constants in prime-related calculations. The proof applies a native decision procedure that evaluates the gcd computation directly.
Claim. $gcd(8,45)=1$
background
This module supplies lightweight wrappers around Mathlib's arithmetic functions, beginning with the Möbius function. The local setting keeps statements minimal to allow later layering of Dirichlet algebra and inversion. The theorem aliases a coprimality fact already present in RSConstants for visibility within prime-related arithmetic.
proof idea
The proof is a one-line wrapper that invokes the native_decide tactic to compute and verify the gcd value equals 1.
why it matters
It earns its place by providing a visible coprimality statement in the arithmetic functions module, which supports Möbius footholds for prime theory. No parent theorems appear in the used_by edges. It touches the basic setup for arithmetic functions without advancing to deeper inversion formulas or 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.