GCD and LCM operations on finsets #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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}
[cancel_comm_monoid_with_zero α]
[normalized_gcd_monoid α]
(s : finset β)
(f : β → α) :
α
Least common multiple of a finite set
Equations
- s.lcm f = finset.fold gcd_monoid.lcm 1 f s
theorem
finset.lcm_def
{α : Type u_1}
{β : Type u_2}
[cancel_comm_monoid_with_zero α]
[normalized_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}
[cancel_comm_monoid_with_zero α]
[normalized_gcd_monoid α]
{f : β → α} :
@[simp]
theorem
finset.lcm_dvd_iff
{α : Type u_1}
{β : Type u_2}
[cancel_comm_monoid_with_zero α]
[normalized_gcd_monoid α]
{s : finset β}
{f : β → α}
{a : α} :
theorem
finset.lcm_dvd
{α : Type u_1}
{β : Type u_2}
[cancel_comm_monoid_with_zero α]
[normalized_gcd_monoid α]
{s : finset β}
{f : β → α}
{a : α} :
theorem
finset.dvd_lcm
{α : Type u_1}
{β : Type u_2}
[cancel_comm_monoid_with_zero α]
[normalized_gcd_monoid α]
{s : finset β}
{f : β → α}
{b : β}
(hb : b ∈ s) :
@[simp]
theorem
finset.lcm_insert
{α : Type u_1}
{β : Type u_2}
[cancel_comm_monoid_with_zero α]
[normalized_gcd_monoid α]
{s : finset β}
{f : β → α}
[decidable_eq β]
{b : β} :
(has_insert.insert b s).lcm f = gcd_monoid.lcm (f b) (s.lcm f)
@[simp]
theorem
finset.lcm_singleton
{α : Type u_1}
{β : Type u_2}
[cancel_comm_monoid_with_zero α]
[normalized_gcd_monoid α]
{f : β → α}
{b : β} :
@[simp]
theorem
finset.normalize_lcm
{α : Type u_1}
{β : Type u_2}
[cancel_comm_monoid_with_zero α]
[normalized_gcd_monoid α]
{s : finset β}
{f : β → α} :
theorem
finset.lcm_union
{α : Type u_1}
{β : Type u_2}
[cancel_comm_monoid_with_zero α]
[normalized_gcd_monoid α]
{s₁ s₂ : finset β}
{f : β → α}
[decidable_eq β] :
theorem
finset.lcm_mono_fun
{α : Type u_1}
{β : Type u_2}
[cancel_comm_monoid_with_zero α]
[normalized_gcd_monoid α]
{s : finset β}
{f g : β → α}
(h : ∀ (b : β), b ∈ s → f b ∣ g b) :
theorem
finset.lcm_mono
{α : Type u_1}
{β : Type u_2}
[cancel_comm_monoid_with_zero α]
[normalized_gcd_monoid α]
{s₁ s₂ : finset β}
{f : β → α}
(h : s₁ ⊆ s₂) :
theorem
finset.lcm_image
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[cancel_comm_monoid_with_zero α]
[normalized_gcd_monoid α]
{f : β → α}
[decidable_eq β]
{g : γ → β}
(s : finset γ) :
(finset.image g s).lcm f = s.lcm (f ∘ g)
theorem
finset.lcm_eq_lcm_image
{α : Type u_1}
{β : Type u_2}
[cancel_comm_monoid_with_zero α]
[normalized_gcd_monoid α]
{s : finset β}
{f : β → α}
[decidable_eq α] :
s.lcm f = (finset.image f s).lcm id
theorem
finset.lcm_eq_zero_iff
{α : Type u_1}
{β : Type u_2}
[cancel_comm_monoid_with_zero α]
[normalized_gcd_monoid α]
{s : finset β}
{f : β → α}
[nontrivial α] :
gcd #
def
finset.gcd
{α : Type u_1}
{β : Type u_2}
[cancel_comm_monoid_with_zero α]
[normalized_gcd_monoid α]
(s : finset β)
(f : β → α) :
α
Greatest common divisor of a finite set
Equations
- s.gcd f = finset.fold gcd_monoid.gcd 0 f s
theorem
finset.gcd_def
{α : Type u_1}
{β : Type u_2}
[cancel_comm_monoid_with_zero α]
[normalized_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}
[cancel_comm_monoid_with_zero α]
[normalized_gcd_monoid α]
{f : β → α} :
theorem
finset.dvd_gcd_iff
{α : Type u_1}
{β : Type u_2}
[cancel_comm_monoid_with_zero α]
[normalized_gcd_monoid α]
{s : finset β}
{f : β → α}
{a : α} :
theorem
finset.gcd_dvd
{α : Type u_1}
{β : Type u_2}
[cancel_comm_monoid_with_zero α]
[normalized_gcd_monoid α]
{s : finset β}
{f : β → α}
{b : β}
(hb : b ∈ s) :
theorem
finset.dvd_gcd
{α : Type u_1}
{β : Type u_2}
[cancel_comm_monoid_with_zero α]
[normalized_gcd_monoid α]
{s : finset β}
{f : β → α}
{a : α} :
@[simp]
theorem
finset.gcd_insert
{α : Type u_1}
{β : Type u_2}
[cancel_comm_monoid_with_zero α]
[normalized_gcd_monoid α]
{s : finset β}
{f : β → α}
[decidable_eq β]
{b : β} :
(has_insert.insert b s).gcd f = gcd_monoid.gcd (f b) (s.gcd f)
@[simp]
theorem
finset.gcd_singleton
{α : Type u_1}
{β : Type u_2}
[cancel_comm_monoid_with_zero α]
[normalized_gcd_monoid α]
{f : β → α}
{b : β} :
@[simp]
theorem
finset.normalize_gcd
{α : Type u_1}
{β : Type u_2}
[cancel_comm_monoid_with_zero α]
[normalized_gcd_monoid α]
{s : finset β}
{f : β → α} :
theorem
finset.gcd_union
{α : Type u_1}
{β : Type u_2}
[cancel_comm_monoid_with_zero α]
[normalized_gcd_monoid α]
{s₁ s₂ : finset β}
{f : β → α}
[decidable_eq β] :
theorem
finset.gcd_mono_fun
{α : Type u_1}
{β : Type u_2}
[cancel_comm_monoid_with_zero α]
[normalized_gcd_monoid α]
{s : finset β}
{f g : β → α}
(h : ∀ (b : β), b ∈ s → f b ∣ g b) :
theorem
finset.gcd_mono
{α : Type u_1}
{β : Type u_2}
[cancel_comm_monoid_with_zero α]
[normalized_gcd_monoid α]
{s₁ s₂ : finset β}
{f : β → α}
(h : s₁ ⊆ s₂) :
theorem
finset.gcd_image
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[cancel_comm_monoid_with_zero α]
[normalized_gcd_monoid α]
{f : β → α}
[decidable_eq β]
{g : γ → β}
(s : finset γ) :
(finset.image g s).gcd f = s.gcd (f ∘ g)
theorem
finset.gcd_eq_gcd_image
{α : Type u_1}
{β : Type u_2}
[cancel_comm_monoid_with_zero α]
[normalized_gcd_monoid α]
{s : finset β}
{f : β → α}
[decidable_eq α] :
s.gcd f = (finset.image f s).gcd id
theorem
finset.gcd_eq_zero_iff
{α : Type u_1}
{β : Type u_2}
[cancel_comm_monoid_with_zero α]
[normalized_gcd_monoid α]
{s : finset β}
{f : β → α} :
theorem
finset.gcd_eq_gcd_filter_ne_zero
{α : Type u_1}
{β : Type u_2}
[cancel_comm_monoid_with_zero α]
[normalized_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}
[cancel_comm_monoid_with_zero α]
[normalized_gcd_monoid α]
{s : finset β}
{f : β → α}
{a : α} :
theorem
finset.gcd_mul_right
{α : Type u_1}
{β : Type u_2}
[cancel_comm_monoid_with_zero α]
[normalized_gcd_monoid α]
{s : finset β}
{f : β → α}
{a : α} :
theorem
finset.gcd_eq_of_dvd_sub
{α : Type u_1}
{β : Type u_2}
[comm_ring α]
[is_domain α]
[normalized_gcd_monoid α]
{s : finset β}
{f g : β → α}
{a : α}
(h : ∀ (x : β), x ∈ s → a ∣ f x - g x) :
gcd_monoid.gcd a (s.gcd f) = gcd_monoid.gcd a (s.gcd g)