mathlib documentation

algebra.gcd_monoid.nat

Basic results about setwise gcds on ℕ #

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

Main results #

@[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