gcd_fortyfive_eight
plain-language theorem explainer
The greatest common divisor of 45 and 8 equals 1. Number theorists checking coprimality inside arithmetic-function developments would cite this fact when verifying squarefree conditions or Möbius inputs. The proof is a one-line native decision that evaluates the gcd by direct computation.
Claim. $ gcd(45, 8) = 1 $
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. Local conventions treat small numerical facts such as this gcd as footholds for divisor counts and squarefree tests. Upstream structures include ledger factorizations that calibrate the J-cost and spectral-emergence results that fix gauge content and fermion counts, though the immediate dependence here runs through the number-theory imports.
proof idea
The proof is a one-line wrapper that applies native_decide to compute the gcd value directly.
why it matters
This supplies a verified coprimality fact inside the arithmetic-functions module that supports the Möbius and squarefree siblings. It fills a basic number-theory slot before Dirichlet inversion layers are added. No downstream theorems are recorded, and it touches the lightweight interface stage described in the module header.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.