Pairwise coprimality

@[reducible, inline]

abbrev PairwiseCoprime {n : ℕ} (a : Fin n → ℤ) : Prop

A predicate stating that the given tuple's numbers are pairwise coprime.

Equations

• PairwiseCoprime a = Pairwise fun (i j : Fin n) => IsCoprime (a i) (a j)

theorem gcd_one_of_pairwiseCoprime {n : ℕ} (hn : 2 ≤ n) {a : Fin n → ℤ} (ha : PairwiseCoprime a) : Finset.univ.gcd a = 1