mathlib documentation

algebra.gcd_monoid.nat

Basic results about setwise gcds on ℕ #

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

Main results #

source
@[protected, instance]
def gcd_monoid.gcd.is_idempotent  :
is_idempotent ℕ gcd
source
theorem finset.coprime_of_div_gcd (s : finset ℕ) {x : ℕ} (hx : x ∈ s) (hnz : x ≠ 0) :
s.gcd (λ (_x : ℕ), _x / s.gcd id) = 1