@[reducible]

def Finset.Coprime (S : Finset ℕ) : Prop

A Finset of numbers is coprime, or relatively prime, if its gcd is 1.

Equations

• S.Coprime = (S.gcd id = 1)

theorem Finset.Coprime_pair_iff (S : Finset ℕ) (a b : ℕ) (h : S = {a, b}) : S.Coprime ↔ a.Coprime b