gcd_threehundredsixty_seven
plain-language theorem explainer
The declaration proves that the greatest common divisor of 360 and 7 equals 1. Number theorists working with arithmetic functions or Möbius inversion in this module cite it to confirm that 7 does not divide 360. The proof applies a single native decision tactic that evaluates the gcd directly.
Claim. $ gcd(360, 7) = 1 $
background
The module supplies lightweight wrappers around Mathlib's arithmetic function library, beginning with the Möbius function μ. Statements remain basic to enable later Dirichlet inversion and squarefree checks. This specific gcd identity supplies a coprimality fact that can support prime-related verifications appearing in sibling definitions such as mobius_prime and mobius_prime_sq.
proof idea
The proof is a one-line wrapper that applies the native_decide tactic to resolve the equality by direct computation.
why it matters
This numerical fact anchors a concrete coprimality check inside the arithmetic functions module. It supports potential downstream use in Möbius function properties for squarefree detection, though no parent theorems or dependents are listed. In the Recognition framework it supplies a basic number-theoretic foothold before layering on deeper inversion or forcing-chain results.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.