# GCD and LCM operations on finsets #

## Main definitions #

• Finset.gcd - the greatest common denominator of a Finset of elements of a GCDMonoid
• Finset.lcm - the least common multiple of a Finset of elements of a GCDMonoid

## Implementation notes #

Many of the proofs use the lemmas gcd_def and lcm_def, which relate Finset.gcd and Finset.lcm to Multiset.gcd and Multiset.lcm.

TODO: simplify with a tactic and Data.Finset.Lattice

## Tags #

finset, gcd

### lcm #

def Finset.lcm {α : Type u_2} {β : Type u_3} (s : ) (f : βα) :
α

Least common multiple of a finite set

Equations
Instances For
theorem Finset.lcm_def {α : Type u_2} {β : Type u_3} {s : } {f : βα} :
s.lcm f = (Multiset.map f s.val).lcm
@[simp]
theorem Finset.lcm_empty {α : Type u_2} {β : Type u_3} {f : βα} :
.lcm f = 1
@[simp]
theorem Finset.lcm_dvd_iff {α : Type u_2} {β : Type u_3} {s : } {f : βα} {a : α} :
s.lcm f a bs, f b a
theorem Finset.lcm_dvd {α : Type u_2} {β : Type u_3} {s : } {f : βα} {a : α} :
(bs, f b a)s.lcm f a
theorem Finset.dvd_lcm {α : Type u_2} {β : Type u_3} {s : } {f : βα} {b : β} (hb : b s) :
f b s.lcm f
@[simp]
theorem Finset.lcm_insert {α : Type u_2} {β : Type u_3} {s : } {f : βα} [] {b : β} :
(insert b s).lcm f = lcm (f b) (s.lcm f)
@[simp]
theorem Finset.lcm_singleton {α : Type u_2} {β : Type u_3} {f : βα} {b : β} :
{b}.lcm f = normalize (f b)
@[simp]
theorem Finset.normalize_lcm {α : Type u_2} {β : Type u_3} {s : } {f : βα} :
normalize (s.lcm f) = s.lcm f
theorem Finset.lcm_union {α : Type u_2} {β : Type u_3} {s₁ : } {s₂ : } {f : βα} [] :
(s₁ s₂).lcm f = lcm (s₁.lcm f) (s₂.lcm f)
theorem Finset.lcm_congr {α : Type u_2} {β : Type u_3} {s₁ : } {s₂ : } {f : βα} {g : βα} (hs : s₁ = s₂) (hfg : as₂, f a = g a) :
s₁.lcm f = s₂.lcm g
theorem Finset.lcm_mono_fun {α : Type u_2} {β : Type u_3} {s : } {f : βα} {g : βα} (h : bs, f b g b) :
s.lcm f s.lcm g
theorem Finset.lcm_mono {α : Type u_2} {β : Type u_3} {s₁ : } {s₂ : } {f : βα} (h : s₁ s₂) :
s₁.lcm f s₂.lcm f
theorem Finset.lcm_image {α : Type u_2} {β : Type u_3} {γ : Type u_4} {f : βα} [] {g : γβ} (s : ) :
().lcm f = s.lcm (f g)
theorem Finset.lcm_eq_lcm_image {α : Type u_2} {β : Type u_3} {s : } {f : βα} [] :
s.lcm f = ().lcm id
theorem Finset.lcm_eq_zero_iff {α : Type u_2} {β : Type u_3} {s : } {f : βα} [] :
s.lcm f = 0 0 f '' s

### gcd #

def Finset.gcd {α : Type u_2} {β : Type u_3} (s : ) (f : βα) :
α

Greatest common divisor of a finite set

Equations
Instances For
theorem Finset.gcd_def {α : Type u_2} {β : Type u_3} {s : } {f : βα} :
s.gcd f = (Multiset.map f s.val).gcd
@[simp]
theorem Finset.gcd_empty {α : Type u_2} {β : Type u_3} {f : βα} :
.gcd f = 0
theorem Finset.dvd_gcd_iff {α : Type u_2} {β : Type u_3} {s : } {f : βα} {a : α} :
a s.gcd f bs, a f b
theorem Finset.gcd_dvd {α : Type u_2} {β : Type u_3} {s : } {f : βα} {b : β} (hb : b s) :
s.gcd f f b
theorem Finset.dvd_gcd {α : Type u_2} {β : Type u_3} {s : } {f : βα} {a : α} :
(bs, a f b)a s.gcd f
@[simp]
theorem Finset.gcd_insert {α : Type u_2} {β : Type u_3} {s : } {f : βα} [] {b : β} :
(insert b s).gcd f = gcd (f b) (s.gcd f)
@[simp]
theorem Finset.gcd_singleton {α : Type u_2} {β : Type u_3} {f : βα} {b : β} :
{b}.gcd f = normalize (f b)
@[simp]
theorem Finset.normalize_gcd {α : Type u_2} {β : Type u_3} {s : } {f : βα} :
normalize (s.gcd f) = s.gcd f
theorem Finset.gcd_union {α : Type u_2} {β : Type u_3} {s₁ : } {s₂ : } {f : βα} [] :
(s₁ s₂).gcd f = gcd (s₁.gcd f) (s₂.gcd f)
theorem Finset.gcd_congr {α : Type u_2} {β : Type u_3} {s₁ : } {s₂ : } {f : βα} {g : βα} (hs : s₁ = s₂) (hfg : as₂, f a = g a) :
s₁.gcd f = s₂.gcd g
theorem Finset.gcd_mono_fun {α : Type u_2} {β : Type u_3} {s : } {f : βα} {g : βα} (h : bs, f b g b) :
s.gcd f s.gcd g
theorem Finset.gcd_mono {α : Type u_2} {β : Type u_3} {s₁ : } {s₂ : } {f : βα} (h : s₁ s₂) :
s₂.gcd f s₁.gcd f
theorem Finset.gcd_image {α : Type u_2} {β : Type u_3} {γ : Type u_4} {f : βα} [] {g : γβ} (s : ) :
().gcd f = s.gcd (f g)
theorem Finset.gcd_eq_gcd_image {α : Type u_2} {β : Type u_3} {s : } {f : βα} [] :
s.gcd f = ().gcd id
theorem Finset.gcd_eq_zero_iff {α : Type u_2} {β : Type u_3} {s : } {f : βα} :
s.gcd f = 0 xs, f x = 0
theorem Finset.gcd_eq_gcd_filter_ne_zero {α : Type u_2} {β : Type u_3} {s : } {f : βα} [DecidablePred fun (x : β) => f x = 0] :
s.gcd f = (Finset.filter (fun (x : β) => f x 0) s).gcd f
theorem Finset.gcd_mul_left {α : Type u_2} {β : Type u_3} {s : } {f : βα} {a : α} :
(s.gcd fun (x : β) => a * f x) = normalize a * s.gcd f
theorem Finset.gcd_mul_right {α : Type u_2} {β : Type u_3} {s : } {f : βα} {a : α} :
(s.gcd fun (x : β) => f x * a) = s.gcd f * normalize a
theorem Finset.extract_gcd' {α : Type u_2} {β : Type u_3} {s : } (f : βα) (g : βα) (hs : xs, f x 0) (hg : bs, f b = s.gcd f * g b) :
s.gcd g = 1
theorem Finset.extract_gcd {α : Type u_2} {β : Type u_3} {s : } (f : βα) (hs : s.Nonempty) :
∃ (g : βα), (bs, f b = s.gcd f * g b) s.gcd g = 1
theorem Finset.gcd_div_eq_one {ι : Type u_1} {α : Type u_2} [Div α] {f : ια} {s : } {i : ι} (his : i s) (hfi : f i 0) :
(s.gcd fun (j : ι) => f j / s.gcd f) = 1

Given a nonempty Finset s and a function f from s to ℕ, if d = s.gcd, then the gcd of (f i) / d is equal to 1.

theorem Finset.gcd_div_id_eq_one {α : Type u_2} [Div α] {s : } {a : α} (has : a s) (ha : a 0) :
(s.gcd fun (b : α) => b / s.gcd id) = 1
theorem Finset.gcd_eq_of_dvd_sub {α : Type u_2} {β : Type u_3} [] [] {s : } {f : βα} {g : βα} {a : α} (h : xs, a f x - g x) :
gcd a (s.gcd f) = gcd a (s.gcd g)