GCD and LCM operations on finsets #
Main definitions #
Finset.gcd- the greatest common denominator of aFinsetof elements of aGCDMonoidFinset.lcm- the least common multiple of aFinsetof elements of aGCDMonoid
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_2}
{β : Type u_3}
[CancelCommMonoidWithZero α]
[NormalizedGCDMonoid α]
(s : Finset β)
(f : β → α)
:
α
Least common multiple of a finite set
Equations
- Finset.lcm s f = Finset.fold lcm 1 f s
Instances For
theorem
Finset.lcm_def
{α : Type u_2}
{β : Type u_3}
[CancelCommMonoidWithZero α]
[NormalizedGCDMonoid α]
{s : Finset β}
{f : β → α}
:
Finset.lcm s f = Multiset.lcm (Multiset.map f s.val)
@[simp]
theorem
Finset.lcm_empty
{α : Type u_2}
{β : Type u_3}
[CancelCommMonoidWithZero α]
[NormalizedGCDMonoid α]
{f : β → α}
:
Finset.lcm ∅ f = 1
@[simp]
theorem
Finset.lcm_dvd_iff
{α : Type u_2}
{β : Type u_3}
[CancelCommMonoidWithZero α]
[NormalizedGCDMonoid α]
{s : Finset β}
{f : β → α}
{a : α}
:
Finset.lcm s f ∣ a ↔ ∀ b ∈ s, f b ∣ a
theorem
Finset.lcm_dvd
{α : Type u_2}
{β : Type u_3}
[CancelCommMonoidWithZero α]
[NormalizedGCDMonoid α]
{s : Finset β}
{f : β → α}
{a : α}
:
(∀ b ∈ s, f b ∣ a) → Finset.lcm s f ∣ a
theorem
Finset.dvd_lcm
{α : Type u_2}
{β : Type u_3}
[CancelCommMonoidWithZero α]
[NormalizedGCDMonoid α]
{s : Finset β}
{f : β → α}
{b : β}
(hb : b ∈ s)
:
f b ∣ Finset.lcm s f
@[simp]
theorem
Finset.lcm_insert
{α : Type u_2}
{β : Type u_3}
[CancelCommMonoidWithZero α]
[NormalizedGCDMonoid α]
{s : Finset β}
{f : β → α}
[DecidableEq β]
{b : β}
:
Finset.lcm (insert b s) f = lcm (f b) (Finset.lcm s f)
@[simp]
theorem
Finset.lcm_singleton
{α : Type u_2}
{β : Type u_3}
[CancelCommMonoidWithZero α]
[NormalizedGCDMonoid α]
{f : β → α}
{b : β}
:
Finset.lcm {b} f = normalize (f b)
@[simp]
theorem
Finset.normalize_lcm
{α : Type u_2}
{β : Type u_3}
[CancelCommMonoidWithZero α]
[NormalizedGCDMonoid α]
{s : Finset β}
{f : β → α}
:
normalize (Finset.lcm s f) = Finset.lcm s f
theorem
Finset.lcm_union
{α : Type u_2}
{β : Type u_3}
[CancelCommMonoidWithZero α]
[NormalizedGCDMonoid α]
{s₁ : Finset β}
{s₂ : Finset β}
{f : β → α}
[DecidableEq β]
:
Finset.lcm (s₁ ∪ s₂) f = lcm (Finset.lcm s₁ f) (Finset.lcm s₂ f)
theorem
Finset.lcm_congr
{α : Type u_2}
{β : Type u_3}
[CancelCommMonoidWithZero α]
[NormalizedGCDMonoid α]
{s₁ : Finset β}
{s₂ : Finset β}
{f : β → α}
{g : β → α}
(hs : s₁ = s₂)
(hfg : ∀ a ∈ s₂, f a = g a)
:
Finset.lcm s₁ f = Finset.lcm s₂ g
theorem
Finset.lcm_mono_fun
{α : Type u_2}
{β : Type u_3}
[CancelCommMonoidWithZero α]
[NormalizedGCDMonoid α]
{s : Finset β}
{f : β → α}
{g : β → α}
(h : ∀ b ∈ s, f b ∣ g b)
:
Finset.lcm s f ∣ Finset.lcm s g
theorem
Finset.lcm_mono
{α : Type u_2}
{β : Type u_3}
[CancelCommMonoidWithZero α]
[NormalizedGCDMonoid α]
{s₁ : Finset β}
{s₂ : Finset β}
{f : β → α}
(h : s₁ ⊆ s₂)
:
Finset.lcm s₁ f ∣ Finset.lcm s₂ f
theorem
Finset.lcm_image
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[CancelCommMonoidWithZero α]
[NormalizedGCDMonoid α]
{f : β → α}
[DecidableEq β]
{g : γ → β}
(s : Finset γ)
:
Finset.lcm (Finset.image g s) f = Finset.lcm s (f ∘ g)
theorem
Finset.lcm_eq_lcm_image
{α : Type u_2}
{β : Type u_3}
[CancelCommMonoidWithZero α]
[NormalizedGCDMonoid α]
{s : Finset β}
{f : β → α}
[DecidableEq α]
:
Finset.lcm s f = Finset.lcm (Finset.image f s) id
theorem
Finset.lcm_eq_zero_iff
{α : Type u_2}
{β : Type u_3}
[CancelCommMonoidWithZero α]
[NormalizedGCDMonoid α]
{s : Finset β}
{f : β → α}
[Nontrivial α]
:
Finset.lcm s f = 0 ↔ 0 ∈ f '' ↑s
gcd #
def
Finset.gcd
{α : Type u_2}
{β : Type u_3}
[CancelCommMonoidWithZero α]
[NormalizedGCDMonoid α]
(s : Finset β)
(f : β → α)
:
α
Greatest common divisor of a finite set
Equations
- Finset.gcd s f = Finset.fold gcd 0 f s
Instances For
theorem
Finset.gcd_def
{α : Type u_2}
{β : Type u_3}
[CancelCommMonoidWithZero α]
[NormalizedGCDMonoid α]
{s : Finset β}
{f : β → α}
:
Finset.gcd s f = Multiset.gcd (Multiset.map f s.val)
@[simp]
theorem
Finset.gcd_empty
{α : Type u_2}
{β : Type u_3}
[CancelCommMonoidWithZero α]
[NormalizedGCDMonoid α]
{f : β → α}
:
Finset.gcd ∅ f = 0
theorem
Finset.dvd_gcd_iff
{α : Type u_2}
{β : Type u_3}
[CancelCommMonoidWithZero α]
[NormalizedGCDMonoid α]
{s : Finset β}
{f : β → α}
{a : α}
:
a ∣ Finset.gcd s f ↔ ∀ b ∈ s, a ∣ f b
theorem
Finset.gcd_dvd
{α : Type u_2}
{β : Type u_3}
[CancelCommMonoidWithZero α]
[NormalizedGCDMonoid α]
{s : Finset β}
{f : β → α}
{b : β}
(hb : b ∈ s)
:
Finset.gcd s f ∣ f b
theorem
Finset.dvd_gcd
{α : Type u_2}
{β : Type u_3}
[CancelCommMonoidWithZero α]
[NormalizedGCDMonoid α]
{s : Finset β}
{f : β → α}
{a : α}
:
(∀ b ∈ s, a ∣ f b) → a ∣ Finset.gcd s f
@[simp]
theorem
Finset.gcd_insert
{α : Type u_2}
{β : Type u_3}
[CancelCommMonoidWithZero α]
[NormalizedGCDMonoid α]
{s : Finset β}
{f : β → α}
[DecidableEq β]
{b : β}
:
Finset.gcd (insert b s) f = gcd (f b) (Finset.gcd s f)
@[simp]
theorem
Finset.gcd_singleton
{α : Type u_2}
{β : Type u_3}
[CancelCommMonoidWithZero α]
[NormalizedGCDMonoid α]
{f : β → α}
{b : β}
:
Finset.gcd {b} f = normalize (f b)
@[simp]
theorem
Finset.normalize_gcd
{α : Type u_2}
{β : Type u_3}
[CancelCommMonoidWithZero α]
[NormalizedGCDMonoid α]
{s : Finset β}
{f : β → α}
:
normalize (Finset.gcd s f) = Finset.gcd s f
theorem
Finset.gcd_union
{α : Type u_2}
{β : Type u_3}
[CancelCommMonoidWithZero α]
[NormalizedGCDMonoid α]
{s₁ : Finset β}
{s₂ : Finset β}
{f : β → α}
[DecidableEq β]
:
Finset.gcd (s₁ ∪ s₂) f = gcd (Finset.gcd s₁ f) (Finset.gcd s₂ f)
theorem
Finset.gcd_congr
{α : Type u_2}
{β : Type u_3}
[CancelCommMonoidWithZero α]
[NormalizedGCDMonoid α]
{s₁ : Finset β}
{s₂ : Finset β}
{f : β → α}
{g : β → α}
(hs : s₁ = s₂)
(hfg : ∀ a ∈ s₂, f a = g a)
:
Finset.gcd s₁ f = Finset.gcd s₂ g
theorem
Finset.gcd_mono_fun
{α : Type u_2}
{β : Type u_3}
[CancelCommMonoidWithZero α]
[NormalizedGCDMonoid α]
{s : Finset β}
{f : β → α}
{g : β → α}
(h : ∀ b ∈ s, f b ∣ g b)
:
Finset.gcd s f ∣ Finset.gcd s g
theorem
Finset.gcd_mono
{α : Type u_2}
{β : Type u_3}
[CancelCommMonoidWithZero α]
[NormalizedGCDMonoid α]
{s₁ : Finset β}
{s₂ : Finset β}
{f : β → α}
(h : s₁ ⊆ s₂)
:
Finset.gcd s₂ f ∣ Finset.gcd s₁ f
theorem
Finset.gcd_image
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[CancelCommMonoidWithZero α]
[NormalizedGCDMonoid α]
{f : β → α}
[DecidableEq β]
{g : γ → β}
(s : Finset γ)
:
Finset.gcd (Finset.image g s) f = Finset.gcd s (f ∘ g)
theorem
Finset.gcd_eq_gcd_image
{α : Type u_2}
{β : Type u_3}
[CancelCommMonoidWithZero α]
[NormalizedGCDMonoid α]
{s : Finset β}
{f : β → α}
[DecidableEq α]
:
Finset.gcd s f = Finset.gcd (Finset.image f s) id
theorem
Finset.gcd_eq_zero_iff
{α : Type u_2}
{β : Type u_3}
[CancelCommMonoidWithZero α]
[NormalizedGCDMonoid α]
{s : Finset β}
{f : β → α}
:
Finset.gcd s f = 0 ↔ ∀ x ∈ s, f x = 0
theorem
Finset.gcd_eq_gcd_filter_ne_zero
{α : Type u_2}
{β : Type u_3}
[CancelCommMonoidWithZero α]
[NormalizedGCDMonoid α]
{s : Finset β}
{f : β → α}
[DecidablePred fun (x : β) => f x = 0]
:
Finset.gcd s f = Finset.gcd (Finset.filter (fun (x : β) => f x ≠ 0) s) f
theorem
Finset.gcd_mul_left
{α : Type u_2}
{β : Type u_3}
[CancelCommMonoidWithZero α]
[NormalizedGCDMonoid α]
{s : Finset β}
{f : β → α}
{a : α}
:
(Finset.gcd s fun (x : β) => a * f x) = normalize a * Finset.gcd s f
theorem
Finset.gcd_mul_right
{α : Type u_2}
{β : Type u_3}
[CancelCommMonoidWithZero α]
[NormalizedGCDMonoid α]
{s : Finset β}
{f : β → α}
{a : α}
:
(Finset.gcd s fun (x : β) => f x * a) = Finset.gcd s f * normalize a
theorem
Finset.extract_gcd'
{α : Type u_2}
{β : Type u_3}
[CancelCommMonoidWithZero α]
[NormalizedGCDMonoid α]
{s : Finset β}
(f : β → α)
(g : β → α)
(hs : ∃ x ∈ s, f x ≠ 0)
(hg : ∀ b ∈ s, f b = Finset.gcd s f * g b)
:
Finset.gcd s g = 1
theorem
Finset.extract_gcd
{α : Type u_2}
{β : Type u_3}
[CancelCommMonoidWithZero α]
[NormalizedGCDMonoid α]
{s : Finset β}
(f : β → α)
(hs : s.Nonempty)
:
∃ (g : β → α), (∀ b ∈ s, f b = Finset.gcd s f * g b) ∧ Finset.gcd s g = 1
theorem
Finset.gcd_div_eq_one
{ι : Type u_1}
{α : Type u_2}
[CancelCommMonoidWithZero α]
[NormalizedGCDMonoid α]
[Div α]
[MulDivCancelClass α]
{f : ι → α}
{s : Finset ι}
{i : ι}
(his : i ∈ s)
(hfi : f i ≠ 0)
:
(Finset.gcd s fun (j : ι) => f j / Finset.gcd s f) = 1
Given a nonempty Finset s and a function f from s to ℕ, if d = s.gcd,
then the gcd of (f i) / d is equal to 1.
theorem
Finset.gcd_div_id_eq_one
{α : Type u_2}
[CancelCommMonoidWithZero α]
[NormalizedGCDMonoid α]
[Div α]
[MulDivCancelClass α]
{s : Finset α}
{a : α}
(has : a ∈ s)
(ha : a ≠ 0)
:
(Finset.gcd s fun (b : α) => b / Finset.gcd s id) = 1
theorem
Finset.gcd_eq_of_dvd_sub
{α : Type u_2}
{β : Type u_3}
[CommRing α]
[IsDomain α]
[NormalizedGCDMonoid α]
{s : Finset β}
{f : β → α}
{g : β → α}
{a : α}
(h : ∀ x ∈ s, a ∣ f x - g x)
:
gcd a (Finset.gcd s f) = gcd a (Finset.gcd s g)