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 #

source

ink

def Multiset.lcm {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : NormalizedGCDMonoid α] (s : Multiset α) :

Least common multiple of a multiset

Equations

Multiset.lcm s = Multiset.fold lcm 1 s

source

ink

@[simp]

theorem Multiset.lcm_zero {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : NormalizedGCDMonoid α] :

Multiset.lcm 0 = 1

source

ink

@[simp]

theorem Multiset.lcm_cons {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : NormalizedGCDMonoid α] (a : α) (s : Multiset α) :

Multiset.lcm (a ::ₘ s) = lcm a (Multiset.lcm s)

source

ink

@[simp]

theorem Multiset.lcm_singleton {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : NormalizedGCDMonoid α] {a : α} :

Multiset.lcm {a} = ↑normalize a

source

ink

@[simp]

theorem Multiset.lcm_add {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : NormalizedGCDMonoid α] (s₁ : Multiset α) (s₂ : Multiset α) :

Multiset.lcm (s₁ + s₂) = lcm (Multiset.lcm s₁) (Multiset.lcm s₂)

source

ink

theorem Multiset.lcm_dvd {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : NormalizedGCDMonoid α] {s : Multiset α} {a : α} :

Multiset.lcm s ∣ a ↔ ∀ (b : α), b ∈ s → b ∣ a

source

ink

theorem Multiset.dvd_lcm {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : NormalizedGCDMonoid α] {s : Multiset α} {a : α} (h : a ∈ s) :

a ∣ Multiset.lcm s

source

ink

theorem Multiset.lcm_mono {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : NormalizedGCDMonoid α] {s₁ : Multiset α} {s₂ : Multiset α} (h : s₁ ⊆ s₂) :

Multiset.lcm s₁ ∣ Multiset.lcm s₂

source

ink

@[simp]

theorem Multiset.normalize_lcm {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : NormalizedGCDMonoid α] (s : Multiset α) :

↑normalize (Multiset.lcm s) = Multiset.lcm s

source

ink

@[simp]

theorem Multiset.lcm_eq_zero_iff {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : NormalizedGCDMonoid α] [inst : Nontrivial α] (s : Multiset α) :

Multiset.lcm s = 0 ↔ 0 ∈ s

source

ink

@[simp]

theorem Multiset.lcm_dedup {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : NormalizedGCDMonoid α] [inst : DecidableEq α] (s : Multiset α) :

Multiset.lcm (Multiset.dedup s) = Multiset.lcm s

source

ink

@[simp]

theorem Multiset.lcm_ndunion {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : NormalizedGCDMonoid α] [inst : DecidableEq α] (s₁ : Multiset α) (s₂ : Multiset α) :

Multiset.lcm (Multiset.ndunion s₁ s₂) = lcm (Multiset.lcm s₁) (Multiset.lcm s₂)

source

ink

@[simp]

theorem Multiset.lcm_union {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : NormalizedGCDMonoid α] [inst : DecidableEq α] (s₁ : Multiset α) (s₂ : Multiset α) :

Multiset.lcm (s₁ ∪ s₂) = lcm (Multiset.lcm s₁) (Multiset.lcm s₂)

source

ink

@[simp]

theorem Multiset.lcm_ndinsert {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : NormalizedGCDMonoid α] [inst : DecidableEq α] (a : α) (s : Multiset α) :

Multiset.lcm (Multiset.ndinsert a s) = lcm a (Multiset.lcm s)

GCD #

source

ink

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

Greatest common divisor of a multiset

Equations

Multiset.gcd s = Multiset.fold gcd 0 s

source

ink

@[simp]

theorem Multiset.gcd_zero {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : NormalizedGCDMonoid α] :

Multiset.gcd 0 = 0

source

ink

@[simp]

theorem Multiset.gcd_cons {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : NormalizedGCDMonoid α] (a : α) (s : Multiset α) :

Multiset.gcd (a ::ₘ s) = gcd a (Multiset.gcd s)

source

ink

@[simp]

theorem Multiset.gcd_singleton {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : NormalizedGCDMonoid α] {a : α} :

Multiset.gcd {a} = ↑normalize a

source

ink

@[simp]

theorem Multiset.gcd_add {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : NormalizedGCDMonoid α] (s₁ : Multiset α) (s₂ : Multiset α) :

Multiset.gcd (s₁ + s₂) = gcd (Multiset.gcd s₁) (Multiset.gcd s₂)

source

ink

theorem Multiset.dvd_gcd {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : NormalizedGCDMonoid α] {s : Multiset α} {a : α} :

a ∣ Multiset.gcd s ↔ ∀ (b : α), b ∈ s → a ∣ b

source

ink

theorem Multiset.gcd_dvd {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : NormalizedGCDMonoid α] {s : Multiset α} {a : α} (h : a ∈ s) :

Multiset.gcd s ∣ a

source

ink

theorem Multiset.gcd_mono {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : NormalizedGCDMonoid α] {s₁ : Multiset α} {s₂ : Multiset α} (h : s₁ ⊆ s₂) :

Multiset.gcd s₂ ∣ Multiset.gcd s₁

source

ink

@[simp]

theorem Multiset.normalize_gcd {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : NormalizedGCDMonoid α] (s : Multiset α) :

↑normalize (Multiset.gcd s) = Multiset.gcd s

source

ink

theorem Multiset.gcd_eq_zero_iff {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : NormalizedGCDMonoid α] (s : Multiset α) :

Multiset.gcd s = 0 ↔ ∀ (x : α), x ∈ s → x = 0

source

ink

theorem Multiset.gcd_map_mul {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : NormalizedGCDMonoid α] (a : α) (s : Multiset α) :

Multiset.gcd (Multiset.map ((fun x x_1 => x * x_1) a) s) = ↑normalize a * Multiset.gcd s

source

ink

@[simp]

theorem Multiset.gcd_dedup {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : NormalizedGCDMonoid α] [inst : DecidableEq α] (s : Multiset α) :

Multiset.gcd (Multiset.dedup s) = Multiset.gcd s

source

ink

@[simp]

theorem Multiset.gcd_ndunion {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : NormalizedGCDMonoid α] [inst : DecidableEq α] (s₁ : Multiset α) (s₂ : Multiset α) :

Multiset.gcd (Multiset.ndunion s₁ s₂) = gcd (Multiset.gcd s₁) (Multiset.gcd s₂)

source

ink

@[simp]

theorem Multiset.gcd_union {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : NormalizedGCDMonoid α] [inst : DecidableEq α] (s₁ : Multiset α) (s₂ : Multiset α) :

Multiset.gcd (s₁ ∪ s₂) = gcd (Multiset.gcd s₁) (Multiset.gcd s₂)

source

ink

@[simp]

theorem Multiset.gcd_ndinsert {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : NormalizedGCDMonoid α] [inst : DecidableEq α] (a : α) (s : Multiset α) :

Multiset.gcd (Multiset.ndinsert a s) = gcd a (Multiset.gcd s)

source

ink

theorem Multiset.extract_gcd' {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : NormalizedGCDMonoid α] (s : Multiset α) (t : Multiset α) (hs : ∃ x, x ∈ s ∧ x ≠ 0) (ht : s = Multiset.map ((fun x x_1 => x * x_1) (Multiset.gcd s)) t) :

Multiset.gcd t = 1

source

ink

theorem Multiset.extract_gcd {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : NormalizedGCDMonoid α] (s : Multiset α) (hs : s ≠ 0) :

∃ t, s = Multiset.map ((fun x x_1 => x * x_1) (Multiset.gcd s)) t ∧ Multiset.gcd t = 1