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

α

Least common multiple of a multiset

Equations

s.lcm = Multiset.fold lcm 1 s

Instances For

@[simp]

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

lcm 0 = 1

@[simp]

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

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

@[simp]

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

{a}.lcm = normalize a

@[simp]

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

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

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

s.lcm ∣ a ↔ ∀ b ∈ s, b ∣ a

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

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

s₁.lcm ∣ s₂.lcm

@[simp]

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

normalize s.lcm = s.lcm

@[simp]

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

s.lcm = 0 ↔ 0 ∈ s

@[simp]

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

s.dedup.lcm = s.lcm

@[simp]

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

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

@[simp]

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

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

@[simp]

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

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

GCD #

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

α

Greatest common divisor of a multiset

Equations

s.gcd = Multiset.fold gcd 0 s

Instances For

@[simp]

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

gcd 0 = 0

@[simp]

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

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

@[simp]

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

{a}.gcd = normalize a

@[simp]

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

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

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

a ∣ s.gcd ↔ ∀ b ∈ s, a ∣ b

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

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

s₂.gcd ∣ s₁.gcd

@[simp]

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

normalize s.gcd = s.gcd

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

s.gcd = 0 ↔ ∀ x ∈ s, x = 0

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

(map (fun (x : α) => a * x) s).gcd = normalize a * s.gcd

@[simp]

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

s.dedup.gcd = s.gcd

@[simp]

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

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

@[simp]

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

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

@[simp]

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

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

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

t.gcd = 1

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

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