GCD and LCM operations on finsets #
Main definitions #
finset.gcd
- the greatest common denominator of afinset
of elements of agcd_monoid
finset.lcm
- the least common multiple of afinset
of 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 : α} :
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 : α} :
@[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₂) :
theorem
finset.gcd_eq_zero_iff
{α : Type u_1}
{β : Type u_2}
[comm_cancel_monoid_with_zero α]
[nontrivial α]
[gcd_monoid α]
{s : finset β}
{f : β → α} :
theorem
finset.gcd_eq_gcd_filter_ne_zero
{α : Type u_1}
{β : Type u_2}
[comm_cancel_monoid_with_zero α]
[nontrivial α]
[gcd_monoid α]
{s : finset β}
{f : β → α}
[decidable_pred (λ (x : β), f x = 0)] :
s.gcd f = (finset.filter (λ (x : β), f x ≠ 0) s).gcd f
theorem
finset.gcd_mul_left
{α : Type u_1}
{β : Type u_2}
[comm_cancel_monoid_with_zero α]
[nontrivial α]
[gcd_monoid α]
{s : finset β}
{f : β → α}
{a : α} :
theorem
finset.gcd_mul_right
{α : Type u_1}
{β : Type u_2}
[comm_cancel_monoid_with_zero α]
[nontrivial α]
[gcd_monoid α]
{s : finset β}
{f : β → α}
{a : α} :
theorem
finset.gcd_eq_of_dvd_sub
{α : Type u_1}
{β : Type u_2}
[nontrivial β]
[integral_domain α]
[gcd_monoid α]
{s : finset β}
{f g : β → α}
{a : α}
(h : ∀ (x : β), x ∈ s → a ∣ f x - g x) :