# mathlibdocumentation

algebra.gcd_monoid.nat

# Basic results about setwise gcds on ℕ #

This file proves some basic results about finset.gcd on ℕ.

## Main results #

• finset.coprime_of_div_gcd: The elements of a set divided through by their gcd are coprime.
@[protected, instance]
theorem finset.coprime_of_div_gcd (s : finset ) {x : } (hx : x s) (hnz : x 0) :
s.gcd (λ (_x : ), _x / s.gcd id) = 1