mathlib documentation

data.multiset.gcd

GCD and LCM operations on multisets

Main definitions

Implementation notes

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

Tags

multiset, gcd

lcm

def multiset.lcm {α : Type u_1} [comm_cancel_monoid_with_zero α] [nontrivial α] [gcd_monoid α] (s : multiset α) :
α

Least common multiple of a multiset

Equations
@[simp]
theorem multiset.lcm_zero {α : Type u_1} [comm_cancel_monoid_with_zero α] [nontrivial α] [gcd_monoid α] :
0.lcm = 1

@[simp]
theorem multiset.lcm_cons {α : Type u_1} [comm_cancel_monoid_with_zero α] [nontrivial α] [gcd_monoid α] (a : α) (s : multiset α) :
(a ::ₘ s).lcm = lcm a s.lcm

@[simp]
theorem multiset.lcm_singleton {α : Type u_1} [comm_cancel_monoid_with_zero α] [nontrivial α] [gcd_monoid α] {a : α} :

@[simp]
theorem multiset.lcm_add {α : Type u_1} [comm_cancel_monoid_with_zero α] [nontrivial α] [gcd_monoid α] (s₁ s₂ : multiset α) :
(s₁ + s₂).lcm = lcm s₁.lcm s₂.lcm

theorem multiset.lcm_dvd {α : Type u_1} [comm_cancel_monoid_with_zero α] [nontrivial α] [gcd_monoid α] {s : multiset α} {a : α} :
s.lcm a ∀ (b : α), b sb a

theorem multiset.dvd_lcm {α : Type u_1} [comm_cancel_monoid_with_zero α] [nontrivial α] [gcd_monoid α] {s : multiset α} {a : α} (h : a s) :
a s.lcm

theorem multiset.lcm_mono {α : Type u_1} [comm_cancel_monoid_with_zero α] [nontrivial α] [gcd_monoid α] {s₁ s₂ : multiset α} (h : s₁ s₂) :
s₁.lcm s₂.lcm

@[simp]
theorem multiset.normalize_lcm {α : Type u_1} [comm_cancel_monoid_with_zero α] [nontrivial α] [gcd_monoid α] (s : multiset α) :

@[simp]
theorem multiset.lcm_erase_dup {α : Type u_1} [comm_cancel_monoid_with_zero α] [nontrivial α] [gcd_monoid α] [decidable_eq α] (s : multiset α) :

@[simp]
theorem multiset.lcm_ndunion {α : Type u_1} [comm_cancel_monoid_with_zero α] [nontrivial α] [gcd_monoid α] [decidable_eq α] (s₁ s₂ : multiset α) :
(s₁.ndunion s₂).lcm = lcm s₁.lcm s₂.lcm

@[simp]
theorem multiset.lcm_union {α : Type u_1} [comm_cancel_monoid_with_zero α] [nontrivial α] [gcd_monoid α] [decidable_eq α] (s₁ s₂ : multiset α) :
(s₁ s₂).lcm = lcm s₁.lcm s₂.lcm

@[simp]
theorem multiset.lcm_ndinsert {α : Type u_1} [comm_cancel_monoid_with_zero α] [nontrivial α] [gcd_monoid α] [decidable_eq α] (a : α) (s : multiset α) :

gcd

def multiset.gcd {α : Type u_1} [comm_cancel_monoid_with_zero α] [nontrivial α] [gcd_monoid α] (s : multiset α) :
α

Greatest common divisor of a multiset

Equations
@[simp]
theorem multiset.gcd_zero {α : Type u_1} [comm_cancel_monoid_with_zero α] [nontrivial α] [gcd_monoid α] :
0.gcd = 0

@[simp]
theorem multiset.gcd_cons {α : Type u_1} [comm_cancel_monoid_with_zero α] [nontrivial α] [gcd_monoid α] (a : α) (s : multiset α) :
(a ::ₘ s).gcd = gcd a s.gcd

@[simp]
theorem multiset.gcd_singleton {α : Type u_1} [comm_cancel_monoid_with_zero α] [nontrivial α] [gcd_monoid α] {a : α} :

@[simp]
theorem multiset.gcd_add {α : Type u_1} [comm_cancel_monoid_with_zero α] [nontrivial α] [gcd_monoid α] (s₁ s₂ : multiset α) :
(s₁ + s₂).gcd = gcd s₁.gcd s₂.gcd

theorem multiset.dvd_gcd {α : Type u_1} [comm_cancel_monoid_with_zero α] [nontrivial α] [gcd_monoid α] {s : multiset α} {a : α} :
a s.gcd ∀ (b : α), b sa b

theorem multiset.gcd_dvd {α : Type u_1} [comm_cancel_monoid_with_zero α] [nontrivial α] [gcd_monoid α] {s : multiset α} {a : α} (h : a s) :
s.gcd a

theorem multiset.gcd_mono {α : Type u_1} [comm_cancel_monoid_with_zero α] [nontrivial α] [gcd_monoid α] {s₁ s₂ : multiset α} (h : s₁ s₂) :
s₂.gcd s₁.gcd

@[simp]
theorem multiset.normalize_gcd {α : Type u_1} [comm_cancel_monoid_with_zero α] [nontrivial α] [gcd_monoid α] (s : multiset α) :

theorem multiset.gcd_eq_zero_iff {α : Type u_1} [comm_cancel_monoid_with_zero α] [nontrivial α] [gcd_monoid α] (s : multiset α) :
s.gcd = 0 ∀ (x : α), x sx = 0

@[simp]
theorem multiset.gcd_erase_dup {α : Type u_1} [comm_cancel_monoid_with_zero α] [nontrivial α] [gcd_monoid α] [decidable_eq α] (s : multiset α) :

@[simp]
theorem multiset.gcd_ndunion {α : Type u_1} [comm_cancel_monoid_with_zero α] [nontrivial α] [gcd_monoid α] [decidable_eq α] (s₁ s₂ : multiset α) :
(s₁.ndunion s₂).gcd = gcd s₁.gcd s₂.gcd

@[simp]
theorem multiset.gcd_union {α : Type u_1} [comm_cancel_monoid_with_zero α] [nontrivial α] [gcd_monoid α] [decidable_eq α] (s₁ s₂ : multiset α) :
(s₁ s₂).gcd = gcd s₁.gcd s₂.gcd

@[simp]
theorem multiset.gcd_ndinsert {α : Type u_1} [comm_cancel_monoid_with_zero α] [nontrivial α] [gcd_monoid α] [decidable_eq α] (a : α) (s : multiset α) :