Documentation

Mathlib.Algebra.GCDMonoid.Multiset

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} [inst : ] [inst : ] (s : ) :
α

Least common multiple of a multiset

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

GCD #

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

Greatest common divisor of a multiset

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