data.finset.gcd

# GCD and LCM operations on finsets #

## Main definitions #

• finset.gcd - the greatest common denominator of a finset of elements of a gcd_monoid
• finset.lcm - the least common multiple of a finset of elements of a gcd_monoid

## 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_1} {β : Type u_2} [nontrivial α] [gcd_monoid α] (s : finset β) (f : β → α) :
α

Least common multiple of a finite set

Equations
theorem finset.lcm_def {α : Type u_1} {β : Type u_2} [nontrivial α] [gcd_monoid α] {s : finset β} {f : β → α} :
s.lcm f = s.val).lcm
@[simp]
theorem finset.lcm_empty {α : Type u_1} {β : Type u_2} [nontrivial α] [gcd_monoid α] {f : β → α} :
.lcm f = 1
@[simp]
theorem finset.lcm_dvd_iff {α : Type u_1} {β : Type u_2} [nontrivial α] [gcd_monoid α] {s : finset β} {f : β → α} {a : α} :
s.lcm f a ∀ (b : β), b sf b a
theorem finset.lcm_dvd {α : Type u_1} {β : Type u_2} [nontrivial α] [gcd_monoid α] {s : finset β} {f : β → α} {a : α} :
(∀ (b : β), b sf b a)s.lcm f a
theorem finset.dvd_lcm {α : Type u_1} {β : Type u_2} [nontrivial α] [gcd_monoid α] {s : finset β} {f : β → α} {b : β} (hb : b s) :
f b s.lcm f
@[simp]
theorem finset.lcm_insert {α : Type u_1} {β : Type u_2} [nontrivial α] [gcd_monoid α] {s : finset β} {f : β → α} [decidable_eq β] {b : β} :
(insert b s).lcm f = lcm (f b) (s.lcm f)
@[simp]
theorem finset.lcm_singleton {α : Type u_1} {β : Type u_2} [nontrivial α] [gcd_monoid α] {f : β → α} {b : β} :
{b}.lcm f = normalize (f b)
@[simp]
theorem finset.normalize_lcm {α : Type u_1} {β : Type u_2} [nontrivial α] [gcd_monoid α] {s : finset β} {f : β → α} :
normalize (s.lcm f) = s.lcm f
theorem finset.lcm_union {α : Type u_1} {β : Type u_2} [nontrivial α] [gcd_monoid α] {s₁ s₂ : finset β} {f : β → α} [decidable_eq β] :
(s₁ s₂).lcm f = lcm (s₁.lcm f) (s₂.lcm f)
theorem finset.lcm_congr {α : Type u_1} {β : Type u_2} [nontrivial α] [gcd_monoid α] {s₁ s₂ : finset β} {f g : β → α} (hs : s₁ = s₂) (hfg : ∀ (a : β), a s₂f a = g a) :
s₁.lcm f = s₂.lcm g
theorem finset.lcm_mono_fun {α : Type u_1} {β : Type u_2} [nontrivial α] [gcd_monoid α] {s : finset β} {f g : β → α} (h : ∀ (b : β), b sf b g b) :
s.lcm f s.lcm g
theorem finset.lcm_mono {α : Type u_1} {β : Type u_2} [nontrivial α] [gcd_monoid α] {s₁ s₂ : finset β} {f : β → α} (h : s₁ s₂) :
s₁.lcm f s₂.lcm f

### gcd #

def finset.gcd {α : Type u_1} {β : Type u_2} [nontrivial α] [gcd_monoid α] (s : finset β) (f : β → α) :
α

Greatest common divisor of a finite set

Equations
theorem finset.gcd_def {α : Type u_1} {β : Type u_2} [nontrivial α] [gcd_monoid α] {s : finset β} {f : β → α} :
s.gcd f = s.val).gcd
@[simp]
theorem finset.gcd_empty {α : Type u_1} {β : Type u_2} [nontrivial α] [gcd_monoid α] {f : β → α} :
.gcd f = 0
theorem finset.dvd_gcd_iff {α : Type u_1} {β : Type u_2} [nontrivial α] [gcd_monoid α] {s : finset β} {f : β → α} {a : α} :
a s.gcd f ∀ (b : β), b sa f b
theorem finset.gcd_dvd {α : Type u_1} {β : Type u_2} [nontrivial α] [gcd_monoid α] {s : finset β} {f : β → α} {b : β} (hb : b s) :
s.gcd f f b
theorem finset.dvd_gcd {α : Type u_1} {β : Type u_2} [nontrivial α] [gcd_monoid α] {s : finset β} {f : β → α} {a : α} :
(∀ (b : β), b sa f b)a s.gcd f
@[simp]
theorem finset.gcd_insert {α : Type u_1} {β : Type u_2} [nontrivial α] [gcd_monoid α] {s : finset β} {f : β → α} [decidable_eq β] {b : β} :
(insert b s).gcd f = gcd (f b) (s.gcd f)
@[simp]
theorem finset.gcd_singleton {α : Type u_1} {β : Type u_2} [nontrivial α] [gcd_monoid α] {f : β → α} {b : β} :
{b}.gcd f = normalize (f b)
@[simp]
theorem finset.normalize_gcd {α : Type u_1} {β : Type u_2} [nontrivial α] [gcd_monoid α] {s : finset β} {f : β → α} :
normalize (s.gcd f) = s.gcd f
theorem finset.gcd_union {α : Type u_1} {β : Type u_2} [nontrivial α] [gcd_monoid α] {s₁ s₂ : finset β} {f : β → α} [decidable_eq β] :
(s₁ s₂).gcd f = gcd (s₁.gcd f) (s₂.gcd f)
theorem finset.gcd_congr {α : Type u_1} {β : Type u_2} [nontrivial α] [gcd_monoid α] {s₁ s₂ : finset β} {f g : β → α} (hs : s₁ = s₂) (hfg : ∀ (a : β), a s₂f a = g a) :
s₁.gcd f = s₂.gcd g
theorem finset.gcd_mono_fun {α : Type u_1} {β : Type u_2} [nontrivial α] [gcd_monoid α] {s : finset β} {f g : β → α} (h : ∀ (b : β), b sf b g b) :
s.gcd f s.gcd g
theorem finset.gcd_mono {α : Type u_1} {β : Type u_2} [nontrivial α] [gcd_monoid α] {s₁ s₂ : finset β} {f : β → α} (h : s₁ s₂) :
s₂.gcd f s₁.gcd f
theorem finset.gcd_eq_zero_iff {α : Type u_1} {β : Type u_2} [nontrivial α] [gcd_monoid α] {s : finset β} {f : β → α} :
s.gcd f = 0 ∀ (x : β), x sf x = 0
theorem finset.gcd_eq_gcd_filter_ne_zero {α : Type u_1} {β : Type u_2} [nontrivial α] [gcd_monoid α] {s : finset β} {f : β → α} [decidable_pred (λ (x : β), f x = 0)] :
s.gcd f = (finset.filter (λ (x : β), f x 0) s).gcd f
theorem finset.gcd_mul_left {α : Type u_1} {β : Type u_2} [nontrivial α] [gcd_monoid α] {s : finset β} {f : β → α} {a : α} :
s.gcd (λ (x : β), a * f x) = (normalize a) * s.gcd f
theorem finset.gcd_mul_right {α : Type u_1} {β : Type u_2} [nontrivial α] [gcd_monoid α] {s : finset β} {f : β → α} {a : α} :
s.gcd (λ (x : β), (f x) * a) = (s.gcd f) *
theorem finset.gcd_eq_of_dvd_sub {α : Type u_1} {β : Type u_2} [nontrivial β] [gcd_monoid α] {s : finset β} {f g : β → α} {a : α} (h : ∀ (x : β), x sa f x - g x) :
gcd a (s.gcd f) = gcd a (s.gcd g)