GCD and LCM operations on finsets
Main definitions
finset.gcd- the greatest common denominator of afinsetof elements of agcd_monoidfinset.lcm- the least common multiple of afinsetof elements of agcd_monoid
Implementation notes
Many of the proofs use the lemmas gcd.def and lcm.def, which relate finset.gcd
and finset.lcm to multiset.gcd and multiset.lcm.
TODO: simplify with a tactic and data.finset.lattice
Tags
finset, gcd
lcm
def
finset.lcm
{α : Type u_1}
{β : Type u_2}
[comm_cancel_monoid_with_zero α]
[nontrivial α]
[gcd_monoid α]
(s : finset β)
(f : β → α) :
α
Least common multiple of a finite set
Equations
- s.lcm f = finset.fold lcm 1 f s
theorem
finset.lcm_def
{α : Type u_1}
{β : Type u_2}
[comm_cancel_monoid_with_zero α]
[nontrivial α]
[gcd_monoid α]
{s : finset β}
{f : β → α} :
s.lcm f = (multiset.map f s.val).lcm
@[simp]
theorem
finset.lcm_empty
{α : Type u_1}
{β : Type u_2}
[comm_cancel_monoid_with_zero α]
[nontrivial α]
[gcd_monoid α]
{f : β → α} :
@[simp]
theorem
finset.lcm_dvd_iff
{α : Type u_1}
{β : Type u_2}
[comm_cancel_monoid_with_zero α]
[nontrivial α]
[gcd_monoid α]
{s : finset β}
{f : β → α}
{a : α} :
theorem
finset.lcm_dvd
{α : Type u_1}
{β : Type u_2}
[comm_cancel_monoid_with_zero α]
[nontrivial α]
[gcd_monoid α]
{s : finset β}
{f : β → α}
{a : α}
(a_1 : ∀ (b : β), b ∈ s → f b ∣ a) :
theorem
finset.dvd_lcm
{α : Type u_1}
{β : Type u_2}
[comm_cancel_monoid_with_zero α]
[nontrivial α]
[gcd_monoid α]
{s : finset β}
{f : β → α}
{b : β}
(hb : b ∈ s) :
@[simp]
theorem
finset.lcm_insert
{α : Type u_1}
{β : Type u_2}
[comm_cancel_monoid_with_zero α]
[nontrivial α]
[gcd_monoid α]
{s : finset β}
{f : β → α}
[decidable_eq β]
{b : β} :
@[simp]
theorem
finset.lcm_singleton
{α : Type u_1}
{β : Type u_2}
[comm_cancel_monoid_with_zero α]
[nontrivial α]
[gcd_monoid α]
{f : β → α}
{b : β} :
@[simp]
theorem
finset.normalize_lcm
{α : Type u_1}
{β : Type u_2}
[comm_cancel_monoid_with_zero α]
[nontrivial α]
[gcd_monoid α]
{s : finset β}
{f : β → α} :
theorem
finset.lcm_union
{α : Type u_1}
{β : Type u_2}
[comm_cancel_monoid_with_zero α]
[nontrivial α]
[gcd_monoid α]
{s₁ s₂ : finset β}
{f : β → α}
[decidable_eq β] :
theorem
finset.lcm_congr
{α : Type u_1}
{β : Type u_2}
[comm_cancel_monoid_with_zero α]
[nontrivial α]
[gcd_monoid α]
{s₁ s₂ : finset β}
{f g : β → α}
(hs : s₁ = s₂)
(hfg : ∀ (a : β), a ∈ s₂ → f a = g a) :
theorem
finset.lcm_mono_fun
{α : Type u_1}
{β : Type u_2}
[comm_cancel_monoid_with_zero α]
[nontrivial α]
[gcd_monoid α]
{s : finset β}
{f g : β → α}
(h : ∀ (b : β), b ∈ s → f b ∣ g b) :
theorem
finset.lcm_mono
{α : Type u_1}
{β : Type u_2}
[comm_cancel_monoid_with_zero α]
[nontrivial α]
[gcd_monoid α]
{s₁ s₂ : finset β}
{f : β → α}
(h : s₁ ⊆ s₂) :
gcd
def
finset.gcd
{α : Type u_1}
{β : Type u_2}
[comm_cancel_monoid_with_zero α]
[nontrivial α]
[gcd_monoid α]
(s : finset β)
(f : β → α) :
α
Greatest common divisor of a finite set
Equations
- s.gcd f = finset.fold gcd 0 f s
theorem
finset.gcd_def
{α : Type u_1}
{β : Type u_2}
[comm_cancel_monoid_with_zero α]
[nontrivial α]
[gcd_monoid α]
{s : finset β}
{f : β → α} :
s.gcd f = (multiset.map f s.val).gcd
@[simp]
theorem
finset.gcd_empty
{α : Type u_1}
{β : Type u_2}
[comm_cancel_monoid_with_zero α]
[nontrivial α]
[gcd_monoid α]
{f : β → α} :
theorem
finset.dvd_gcd_iff
{α : Type u_1}
{β : Type u_2}
[comm_cancel_monoid_with_zero α]
[nontrivial α]
[gcd_monoid α]
{s : finset β}
{f : β → α}
{a : α} :
theorem
finset.gcd_dvd
{α : Type u_1}
{β : Type u_2}
[comm_cancel_monoid_with_zero α]
[nontrivial α]
[gcd_monoid α]
{s : finset β}
{f : β → α}
{b : β}
(hb : b ∈ s) :
theorem
finset.dvd_gcd
{α : Type u_1}
{β : Type u_2}
[comm_cancel_monoid_with_zero α]
[nontrivial α]
[gcd_monoid α]
{s : finset β}
{f : β → α}
{a : α}
(a_1 : ∀ (b : β), b ∈ s → a ∣ f b) :
@[simp]
theorem
finset.gcd_insert
{α : Type u_1}
{β : Type u_2}
[comm_cancel_monoid_with_zero α]
[nontrivial α]
[gcd_monoid α]
{s : finset β}
{f : β → α}
[decidable_eq β]
{b : β} :
@[simp]
theorem
finset.gcd_singleton
{α : Type u_1}
{β : Type u_2}
[comm_cancel_monoid_with_zero α]
[nontrivial α]
[gcd_monoid α]
{f : β → α}
{b : β} :
@[simp]
theorem
finset.normalize_gcd
{α : Type u_1}
{β : Type u_2}
[comm_cancel_monoid_with_zero α]
[nontrivial α]
[gcd_monoid α]
{s : finset β}
{f : β → α} :
theorem
finset.gcd_union
{α : Type u_1}
{β : Type u_2}
[comm_cancel_monoid_with_zero α]
[nontrivial α]
[gcd_monoid α]
{s₁ s₂ : finset β}
{f : β → α}
[decidable_eq β] :
theorem
finset.gcd_congr
{α : Type u_1}
{β : Type u_2}
[comm_cancel_monoid_with_zero α]
[nontrivial α]
[gcd_monoid α]
{s₁ s₂ : finset β}
{f g : β → α}
(hs : s₁ = s₂)
(hfg : ∀ (a : β), a ∈ s₂ → f a = g a) :
theorem
finset.gcd_mono_fun
{α : Type u_1}
{β : Type u_2}
[comm_cancel_monoid_with_zero α]
[nontrivial α]
[gcd_monoid α]
{s : finset β}
{f g : β → α}
(h : ∀ (b : β), b ∈ s → f b ∣ g b) :
theorem
finset.gcd_mono
{α : Type u_1}
{β : Type u_2}
[comm_cancel_monoid_with_zero α]
[nontrivial α]
[gcd_monoid α]
{s₁ s₂ : finset β}
{f : β → α}
(h : s₁ ⊆ s₂) :