mathlib3 documentation

algebra.gcd_monoid.multiset

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 #

Implementation notes #

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

Tags #

multiset, gcd

lcm #

Least common multiple of a multiset

Equations
@[simp]
theorem multiset.lcm_cons {α : Type u_1} [cancel_comm_monoid_with_zero α] [normalized_gcd_monoid α] (a : α) (s : multiset α) :
@[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
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
theorem multiset.dvd_lcm {α : Type u_1} [cancel_comm_monoid_with_zero α] [normalized_gcd_monoid α] {s : multiset α} {a : α} (h : a s) :
a s.lcm
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
@[simp]
@[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
@[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

gcd #

Greatest common divisor of a multiset

Equations
@[simp]
theorem multiset.gcd_cons {α : Type u_1} [cancel_comm_monoid_with_zero α] [normalized_gcd_monoid α] (a : α) (s : multiset α) :
@[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
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
theorem multiset.gcd_dvd {α : Type u_1} [cancel_comm_monoid_with_zero α] [normalized_gcd_monoid α] {s : multiset α} {a : α} (h : a s) :
s.gcd a
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
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
@[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
@[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
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