GCD and LCM operations on multisets #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Main definitions #

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

Implementation notes #

TODO: simplify with a tactic and data.multiset.lattice

Tags #

multiset, gcd

lcm #

source

def multiset.lcm {α : Type u_1} [cancel_comm_monoid_with_zero α] [normalized_gcd_monoid α] (s : multiset α) :

Least common multiple of a multiset

Equations

s.lcm = multiset.fold gcd_monoid.lcm 1 s

source

@[simp]

theorem multiset.lcm_zero {α : Type u_1} [cancel_comm_monoid_with_zero α] [normalized_gcd_monoid α] :

0.lcm = 1

source

@[simp]

theorem multiset.lcm_cons {α : Type u_1} [cancel_comm_monoid_with_zero α] [normalized_gcd_monoid α] (a : α) (s : multiset α) :

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

source

@[simp]

theorem multiset.lcm_singleton {α : Type u_1} [cancel_comm_monoid_with_zero α] [normalized_gcd_monoid α] {a : α} :

{a}.lcm = ⇑normalize a

source

@[simp]

theorem multiset.lcm_add {α : Type u_1} [cancel_comm_monoid_with_zero α] [normalized_gcd_monoid α] (s₁ s₂ : multiset α) :

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

source

theorem multiset.lcm_dvd {α : Type u_1} [cancel_comm_monoid_with_zero α] [normalized_gcd_monoid α] {s : multiset α} {a : α} :

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

source

theorem multiset.dvd_lcm {α : Type u_1} [cancel_comm_monoid_with_zero α] [normalized_gcd_monoid α] {s : multiset α} {a : α} (h : a ∈ s) :

a ∣ s.lcm

source

theorem multiset.lcm_mono {α : Type u_1} [cancel_comm_monoid_with_zero α] [normalized_gcd_monoid α] {s₁ s₂ : multiset α} (h : s₁ ⊆ s₂) :

s₁.lcm ∣ s₂.lcm

source

@[simp]

theorem multiset.normalize_lcm {α : Type u_1} [cancel_comm_monoid_with_zero α] [normalized_gcd_monoid α] (s : multiset α) :

⇑normalize s.lcm = s.lcm

source

@[simp]

theorem multiset.lcm_eq_zero_iff {α : Type u_1} [cancel_comm_monoid_with_zero α] [normalized_gcd_monoid α] [nontrivial α] (s : multiset α) :

s.lcm = 0 ↔ 0 ∈ s

source

@[simp]

theorem multiset.lcm_dedup {α : Type u_1} [cancel_comm_monoid_with_zero α] [normalized_gcd_monoid α] [decidable_eq α] (s : multiset α) :

s.dedup.lcm = s.lcm

source

@[simp]

theorem multiset.lcm_ndunion {α : Type u_1} [cancel_comm_monoid_with_zero α] [normalized_gcd_monoid α] [decidable_eq α] (s₁ s₂ : multiset α) :

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

source

@[simp]

theorem multiset.lcm_union {α : Type u_1} [cancel_comm_monoid_with_zero α] [normalized_gcd_monoid α] [decidable_eq α] (s₁ s₂ : multiset α) :

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

source

@[simp]

theorem multiset.lcm_ndinsert {α : Type u_1} [cancel_comm_monoid_with_zero α] [normalized_gcd_monoid α] [decidable_eq α] (a : α) (s : multiset α) :

(multiset.ndinsert a s).lcm = gcd_monoid.lcm a s.lcm

gcd #

source

def multiset.gcd {α : Type u_1} [cancel_comm_monoid_with_zero α] [normalized_gcd_monoid α] (s : multiset α) :

Greatest common divisor of a multiset

Equations

s.gcd = multiset.fold gcd_monoid.gcd 0 s

source

@[simp]

theorem multiset.gcd_zero {α : Type u_1} [cancel_comm_monoid_with_zero α] [normalized_gcd_monoid α] :

0.gcd = 0

source

@[simp]

theorem multiset.gcd_cons {α : Type u_1} [cancel_comm_monoid_with_zero α] [normalized_gcd_monoid α] (a : α) (s : multiset α) :

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

source

@[simp]

theorem multiset.gcd_singleton {α : Type u_1} [cancel_comm_monoid_with_zero α] [normalized_gcd_monoid α] {a : α} :

{a}.gcd = ⇑normalize a

source

@[simp]

theorem multiset.gcd_add {α : Type u_1} [cancel_comm_monoid_with_zero α] [normalized_gcd_monoid α] (s₁ s₂ : multiset α) :

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

source

theorem multiset.dvd_gcd {α : Type u_1} [cancel_comm_monoid_with_zero α] [normalized_gcd_monoid α] {s : multiset α} {a : α} :

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

source

theorem multiset.gcd_dvd {α : Type u_1} [cancel_comm_monoid_with_zero α] [normalized_gcd_monoid α] {s : multiset α} {a : α} (h : a ∈ s) :

s.gcd ∣ a

source

theorem multiset.gcd_mono {α : Type u_1} [cancel_comm_monoid_with_zero α] [normalized_gcd_monoid α] {s₁ s₂ : multiset α} (h : s₁ ⊆ s₂) :

s₂.gcd ∣ s₁.gcd

source

@[simp]

theorem multiset.normalize_gcd {α : Type u_1} [cancel_comm_monoid_with_zero α] [normalized_gcd_monoid α] (s : multiset α) :

⇑normalize s.gcd = s.gcd

source

theorem multiset.gcd_eq_zero_iff {α : Type u_1} [cancel_comm_monoid_with_zero α] [normalized_gcd_monoid α] (s : multiset α) :

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

source

theorem multiset.gcd_map_mul {α : Type u_1} [cancel_comm_monoid_with_zero α] [normalized_gcd_monoid α] (a : α) (s : multiset α) :

(multiset.map (has_mul.mul a) s).gcd = ⇑normalize a * s.gcd

source

@[simp]

theorem multiset.gcd_dedup {α : Type u_1} [cancel_comm_monoid_with_zero α] [normalized_gcd_monoid α] [decidable_eq α] (s : multiset α) :

s.dedup.gcd = s.gcd

source

@[simp]

theorem multiset.gcd_ndunion {α : Type u_1} [cancel_comm_monoid_with_zero α] [normalized_gcd_monoid α] [decidable_eq α] (s₁ s₂ : multiset α) :

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

source

@[simp]

theorem multiset.gcd_union {α : Type u_1} [cancel_comm_monoid_with_zero α] [normalized_gcd_monoid α] [decidable_eq α] (s₁ s₂ : multiset α) :

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

source

@[simp]

theorem multiset.gcd_ndinsert {α : Type u_1} [cancel_comm_monoid_with_zero α] [normalized_gcd_monoid α] [decidable_eq α] (a : α) (s : multiset α) :

(multiset.ndinsert a s).gcd = gcd_monoid.gcd a s.gcd

source

theorem multiset.extract_gcd' {α : Type u_1} [cancel_comm_monoid_with_zero α] [normalized_gcd_monoid α] (s t : multiset α) (hs : ∃ (x : α), x ∈ s ∧ x ≠ 0) (ht : s = multiset.map (has_mul.mul s.gcd) t) :

t.gcd = 1

source

theorem multiset.extract_gcd {α : Type u_1} [cancel_comm_monoid_with_zero α] [normalized_gcd_monoid α] (s : multiset α) (hs : s ≠ 0) :

∃ (t : multiset α), s = multiset.map (has_mul.mul s.gcd) t ∧ t.gcd = 1