# GCD and LCM operations on multisets #

## Main definitions #

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

## Implementation notes #

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

## Tags #

multiset, gcd

### LCM #

def Multiset.lcm {α : Type u_1} (s : ) :
α

Least common multiple of a multiset

Equations
Instances For
@[simp]
theorem Multiset.lcm_zero {α : Type u_1} :
@[simp]
theorem Multiset.lcm_cons {α : Type u_1} (a : α) (s : ) :
(a ::ₘ s).lcm = lcm a s.lcm
@[simp]
theorem Multiset.lcm_singleton {α : Type u_1} {a : α} :
{a}.lcm = normalize a
@[simp]
theorem Multiset.lcm_add {α : Type u_1} (s₁ : ) (s₂ : ) :
(s₁ + s₂).lcm = lcm s₁.lcm s₂.lcm
theorem Multiset.lcm_dvd {α : Type u_1} {s : } {a : α} :
s.lcm a bs, b a
theorem Multiset.dvd_lcm {α : Type u_1} {s : } {a : α} (h : a s) :
a s.lcm
theorem Multiset.lcm_mono {α : Type u_1} {s₁ : } {s₂ : } (h : s₁ s₂) :
s₁.lcm s₂.lcm
@[simp]
theorem Multiset.normalize_lcm {α : Type u_1} (s : ) :
normalize s.lcm = s.lcm
@[simp]
theorem Multiset.lcm_eq_zero_iff {α : Type u_1} [] (s : ) :
s.lcm = 0 0 s
@[simp]
theorem Multiset.lcm_dedup {α : Type u_1} [] (s : ) :
s.dedup.lcm = s.lcm
@[simp]
theorem Multiset.lcm_ndunion {α : Type u_1} [] (s₁ : ) (s₂ : ) :
(s₁.ndunion s₂).lcm = lcm s₁.lcm s₂.lcm
@[simp]
theorem Multiset.lcm_union {α : Type u_1} [] (s₁ : ) (s₂ : ) :
(s₁ s₂).lcm = lcm s₁.lcm s₂.lcm
@[simp]
theorem Multiset.lcm_ndinsert {α : Type u_1} [] (a : α) (s : ) :
().lcm = lcm a s.lcm

### GCD #

def Multiset.gcd {α : Type u_1} (s : ) :
α

Greatest common divisor of a multiset

Equations
Instances For
@[simp]
theorem Multiset.gcd_zero {α : Type u_1} :
@[simp]
theorem Multiset.gcd_cons {α : Type u_1} (a : α) (s : ) :
(a ::ₘ s).gcd = gcd a s.gcd
@[simp]
theorem Multiset.gcd_singleton {α : Type u_1} {a : α} :
{a}.gcd = normalize a
@[simp]
theorem Multiset.gcd_add {α : Type u_1} (s₁ : ) (s₂ : ) :
(s₁ + s₂).gcd = gcd s₁.gcd s₂.gcd
theorem Multiset.dvd_gcd {α : Type u_1} {s : } {a : α} :
a s.gcd bs, a b
theorem Multiset.gcd_dvd {α : Type u_1} {s : } {a : α} (h : a s) :
s.gcd a
theorem Multiset.gcd_mono {α : Type u_1} {s₁ : } {s₂ : } (h : s₁ s₂) :
s₂.gcd s₁.gcd
@[simp]
theorem Multiset.normalize_gcd {α : Type u_1} (s : ) :
normalize s.gcd = s.gcd
theorem Multiset.gcd_eq_zero_iff {α : Type u_1} (s : ) :
s.gcd = 0 xs, x = 0
theorem Multiset.gcd_map_mul {α : Type u_1} (a : α) (s : ) :
(Multiset.map (fun (x : α) => a * x) s).gcd = normalize a * s.gcd
@[simp]
theorem Multiset.gcd_dedup {α : Type u_1} [] (s : ) :
s.dedup.gcd = s.gcd
@[simp]
theorem Multiset.gcd_ndunion {α : Type u_1} [] (s₁ : ) (s₂ : ) :
(s₁.ndunion s₂).gcd = gcd s₁.gcd s₂.gcd
@[simp]
theorem Multiset.gcd_union {α : Type u_1} [] (s₁ : ) (s₂ : ) :
(s₁ s₂).gcd = gcd s₁.gcd s₂.gcd
@[simp]
theorem Multiset.gcd_ndinsert {α : Type u_1} [] (a : α) (s : ) :
().gcd = gcd a s.gcd
theorem Multiset.extract_gcd' {α : Type u_1} (s : ) (t : ) (hs : xs, x 0) (ht : s = Multiset.map (fun (x : α) => s.gcd * x) t) :
t.gcd = 1
theorem Multiset.extract_gcd {α : Type u_1} (s : ) (hs : s 0) :
∃ (t : ), s = Multiset.map (fun (x : α) => s.gcd * x) t t.gcd = 1