Theorem Int.isCoprime_gcdA

Modification history

2025-12-07 12:35

Mathlib/RingTheory/Coprime/Lemmas.lean

feat(RingTheory/Coprime/Lemmas): Add Int.isCoprime_gcdA/B (#32369) …

Added Int.isCoprime_gcdA View on Github →