GCD and LCM operations on multisets #
Main definitions #
multiset.gcd
- the greatest common denominator of amultiset
of elements of agcd_monoid
multiset.lcm
- the least common multiple of amultiset
of elements of agcd_monoid
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
- s.lcm = multiset.fold lcm 1 s
@[simp]
theorem
multiset.lcm_zero
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[nontrivial α]
[gcd_monoid α] :
@[simp]
theorem
multiset.lcm_cons
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[nontrivial α]
[gcd_monoid α]
(a : α)
(s : multiset α) :
@[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 α) :
theorem
multiset.lcm_dvd
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[nontrivial α]
[gcd_monoid α]
{s : multiset α}
{a : α} :
theorem
multiset.dvd_lcm
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[nontrivial α]
[gcd_monoid α]
{s : multiset α}
{a : α}
(h : a ∈ s) :
theorem
multiset.lcm_mono
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[nontrivial α]
[gcd_monoid α]
{s₁ s₂ : multiset α}
(h : s₁ ⊆ s₂) :
@[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 α) :
@[simp]
theorem
multiset.lcm_union
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[nontrivial α]
[gcd_monoid α]
[decidable_eq α]
(s₁ s₂ : multiset α) :
@[simp]
theorem
multiset.lcm_ndinsert
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[nontrivial α]
[gcd_monoid α]
[decidable_eq α]
(a : α)
(s : multiset α) :
(multiset.ndinsert a s).lcm = lcm a s.lcm
gcd #
def
multiset.gcd
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[nontrivial α]
[gcd_monoid α]
(s : multiset α) :
α
Greatest common divisor of a multiset
Equations
- s.gcd = multiset.fold gcd 0 s
@[simp]
theorem
multiset.gcd_zero
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[nontrivial α]
[gcd_monoid α] :
@[simp]
theorem
multiset.gcd_cons
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[nontrivial α]
[gcd_monoid α]
(a : α)
(s : multiset α) :
@[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 α) :
theorem
multiset.dvd_gcd
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[nontrivial α]
[gcd_monoid α]
{s : multiset α}
{a : α} :
theorem
multiset.gcd_dvd
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[nontrivial α]
[gcd_monoid α]
{s : multiset α}
{a : α}
(h : a ∈ s) :
theorem
multiset.gcd_mono
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[nontrivial α]
[gcd_monoid α]
{s₁ s₂ : multiset α}
(h : s₁ ⊆ s₂) :
@[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 α) :
@[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 α) :
@[simp]
theorem
multiset.gcd_union
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[nontrivial α]
[gcd_monoid α]
[decidable_eq α]
(s₁ s₂ : multiset α) :
@[simp]
theorem
multiset.gcd_ndinsert
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[nontrivial α]
[gcd_monoid α]
[decidable_eq α]
(a : α)
(s : multiset α) :
(multiset.ndinsert a s).gcd = gcd a s.gcd