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_1}
{β : Type u_2}
[inst : CancelCommMonoidWithZero α]
[inst : NormalizedGCDMonoid α]
(s : Finset β)
(f : β → α)
:
α
Least common multiple of a finite set
Equations
- Finset.lcm s f = Finset.fold lcm 1 f s
theorem
Finset.lcm_def
{α : Type u_1}
{β : Type u_2}
[inst : CancelCommMonoidWithZero α]
[inst : NormalizedGCDMonoid α]
{s : Finset β}
{f : β → α}
:
Finset.lcm s f = Multiset.lcm (Multiset.map f s.val)
@[simp]
theorem
Finset.lcm_empty
{α : Type u_1}
{β : Type u_2}
[inst : CancelCommMonoidWithZero α]
[inst : NormalizedGCDMonoid α]
{f : β → α}
:
Finset.lcm ∅ f = 1
@[simp]
theorem
Finset.lcm_dvd_iff
{α : Type u_1}
{β : Type u_2}
[inst : CancelCommMonoidWithZero α]
[inst : NormalizedGCDMonoid α]
{s : Finset β}
{f : β → α}
{a : α}
:
Finset.lcm s f ∣ a ↔ ∀ (b : β), b ∈ s → f b ∣ a
theorem
Finset.lcm_dvd
{α : Type u_2}
{β : Type u_1}
[inst : CancelCommMonoidWithZero α]
[inst : NormalizedGCDMonoid α]
{s : Finset β}
{f : β → α}
{a : α}
:
(∀ (b : β), b ∈ s → f b ∣ a) → Finset.lcm s f ∣ a
theorem
Finset.dvd_lcm
{α : Type u_2}
{β : Type u_1}
[inst : CancelCommMonoidWithZero α]
[inst : NormalizedGCDMonoid α]
{s : Finset β}
{f : β → α}
{b : β}
(hb : b ∈ s)
:
f b ∣ Finset.lcm s f
@[simp]
theorem
Finset.lcm_insert
{α : Type u_2}
{β : Type u_1}
[inst : CancelCommMonoidWithZero α]
[inst : NormalizedGCDMonoid α]
{s : Finset β}
{f : β → α}
[inst : DecidableEq β]
{b : β}
:
Finset.lcm (insert b s) f = lcm (f b) (Finset.lcm s f)
@[simp]
theorem
Finset.lcm_singleton
{α : Type u_1}
{β : Type u_2}
[inst : CancelCommMonoidWithZero α]
[inst : NormalizedGCDMonoid α]
{f : β → α}
{b : β}
:
Finset.lcm {b} f = ↑normalize (f b)
@[simp]
theorem
Finset.normalize_lcm
{α : Type u_1}
{β : Type u_2}
[inst : CancelCommMonoidWithZero α]
[inst : NormalizedGCDMonoid α]
{s : Finset β}
{f : β → α}
:
↑normalize (Finset.lcm s f) = Finset.lcm s f
theorem
Finset.lcm_union
{α : Type u_2}
{β : Type u_1}
[inst : CancelCommMonoidWithZero α]
[inst : NormalizedGCDMonoid α]
{s₁ : Finset β}
{s₂ : Finset β}
{f : β → α}
[inst : DecidableEq β]
:
Finset.lcm (s₁ ∪ s₂) f = lcm (Finset.lcm s₁ f) (Finset.lcm s₂ f)
theorem
Finset.lcm_congr
{α : Type u_2}
{β : Type u_1}
[inst : CancelCommMonoidWithZero α]
[inst : NormalizedGCDMonoid α]
{s₁ : Finset β}
{s₂ : Finset β}
{f : β → α}
{g : β → α}
(hs : s₁ = s₂)
(hfg : ∀ (a : β), a ∈ s₂ → f a = g a)
:
Finset.lcm s₁ f = Finset.lcm s₂ g
theorem
Finset.lcm_mono_fun
{α : Type u_2}
{β : Type u_1}
[inst : CancelCommMonoidWithZero α]
[inst : NormalizedGCDMonoid α]
{s : Finset β}
{f : β → α}
{g : β → α}
(h : ∀ (b : β), b ∈ s → f b ∣ g b)
:
Finset.lcm s f ∣ Finset.lcm s g
theorem
Finset.lcm_mono
{α : Type u_2}
{β : Type u_1}
[inst : CancelCommMonoidWithZero α]
[inst : NormalizedGCDMonoid α]
{s₁ : Finset β}
{s₂ : Finset β}
{f : β → α}
(h : s₁ ⊆ s₂)
:
Finset.lcm s₁ f ∣ Finset.lcm s₂ f
theorem
Finset.lcm_image
{α : Type u_3}
{β : Type u_1}
{γ : Type u_2}
[inst : CancelCommMonoidWithZero α]
[inst : NormalizedGCDMonoid α]
{f : β → α}
[inst : DecidableEq β]
{g : γ → β}
(s : Finset γ)
:
Finset.lcm (Finset.image g s) f = Finset.lcm s (f ∘ g)
theorem
Finset.lcm_eq_lcm_image
{α : Type u_1}
{β : Type u_2}
[inst : CancelCommMonoidWithZero α]
[inst : NormalizedGCDMonoid α]
{s : Finset β}
{f : β → α}
[inst : DecidableEq α]
:
Finset.lcm s f = Finset.lcm (Finset.image f s) id
theorem
Finset.lcm_eq_zero_iff
{α : Type u_1}
{β : Type u_2}
[inst : CancelCommMonoidWithZero α]
[inst : NormalizedGCDMonoid α]
{s : Finset β}
{f : β → α}
[inst : Nontrivial α]
:
Finset.lcm s f = 0 ↔ 0 ∈ f '' ↑s
gcd #
def
Finset.gcd
{α : Type u_1}
{β : Type u_2}
[inst : CancelCommMonoidWithZero α]
[inst : NormalizedGCDMonoid α]
(s : Finset β)
(f : β → α)
:
α
Greatest common divisor of a finite set
Equations
- Finset.gcd s f = Finset.fold gcd 0 f s
theorem
Finset.gcd_def
{α : Type u_1}
{β : Type u_2}
[inst : CancelCommMonoidWithZero α]
[inst : NormalizedGCDMonoid α]
{s : Finset β}
{f : β → α}
:
Finset.gcd s f = Multiset.gcd (Multiset.map f s.val)
@[simp]
theorem
Finset.gcd_empty
{α : Type u_1}
{β : Type u_2}
[inst : CancelCommMonoidWithZero α]
[inst : NormalizedGCDMonoid α]
{f : β → α}
:
Finset.gcd ∅ f = 0
theorem
Finset.dvd_gcd_iff
{α : Type u_1}
{β : Type u_2}
[inst : CancelCommMonoidWithZero α]
[inst : NormalizedGCDMonoid α]
{s : Finset β}
{f : β → α}
{a : α}
:
a ∣ Finset.gcd s f ↔ ∀ (b : β), b ∈ s → a ∣ f b
theorem
Finset.gcd_dvd
{α : Type u_2}
{β : Type u_1}
[inst : CancelCommMonoidWithZero α]
[inst : NormalizedGCDMonoid α]
{s : Finset β}
{f : β → α}
{b : β}
(hb : b ∈ s)
:
Finset.gcd s f ∣ f b
theorem
Finset.dvd_gcd
{α : Type u_2}
{β : Type u_1}
[inst : CancelCommMonoidWithZero α]
[inst : NormalizedGCDMonoid α]
{s : Finset β}
{f : β → α}
{a : α}
:
(∀ (b : β), b ∈ s → a ∣ f b) → a ∣ Finset.gcd s f
@[simp]
theorem
Finset.gcd_insert
{α : Type u_2}
{β : Type u_1}
[inst : CancelCommMonoidWithZero α]
[inst : NormalizedGCDMonoid α]
{s : Finset β}
{f : β → α}
[inst : DecidableEq β]
{b : β}
:
Finset.gcd (insert b s) f = gcd (f b) (Finset.gcd s f)
@[simp]
theorem
Finset.gcd_singleton
{α : Type u_1}
{β : Type u_2}
[inst : CancelCommMonoidWithZero α]
[inst : NormalizedGCDMonoid α]
{f : β → α}
{b : β}
:
Finset.gcd {b} f = ↑normalize (f b)
@[simp]
theorem
Finset.normalize_gcd
{α : Type u_1}
{β : Type u_2}
[inst : CancelCommMonoidWithZero α]
[inst : NormalizedGCDMonoid α]
{s : Finset β}
{f : β → α}
:
↑normalize (Finset.gcd s f) = Finset.gcd s f
theorem
Finset.gcd_union
{α : Type u_2}
{β : Type u_1}
[inst : CancelCommMonoidWithZero α]
[inst : NormalizedGCDMonoid α]
{s₁ : Finset β}
{s₂ : Finset β}
{f : β → α}
[inst : DecidableEq β]
:
Finset.gcd (s₁ ∪ s₂) f = gcd (Finset.gcd s₁ f) (Finset.gcd s₂ f)
theorem
Finset.gcd_congr
{α : Type u_2}
{β : Type u_1}
[inst : CancelCommMonoidWithZero α]
[inst : NormalizedGCDMonoid α]
{s₁ : Finset β}
{s₂ : Finset β}
{f : β → α}
{g : β → α}
(hs : s₁ = s₂)
(hfg : ∀ (a : β), a ∈ s₂ → f a = g a)
:
Finset.gcd s₁ f = Finset.gcd s₂ g
theorem
Finset.gcd_mono_fun
{α : Type u_2}
{β : Type u_1}
[inst : CancelCommMonoidWithZero α]
[inst : NormalizedGCDMonoid α]
{s : Finset β}
{f : β → α}
{g : β → α}
(h : ∀ (b : β), b ∈ s → f b ∣ g b)
:
Finset.gcd s f ∣ Finset.gcd s g
theorem
Finset.gcd_mono
{α : Type u_2}
{β : Type u_1}
[inst : CancelCommMonoidWithZero α]
[inst : NormalizedGCDMonoid α]
{s₁ : Finset β}
{s₂ : Finset β}
{f : β → α}
(h : s₁ ⊆ s₂)
:
Finset.gcd s₂ f ∣ Finset.gcd s₁ f
theorem
Finset.gcd_image
{α : Type u_3}
{β : Type u_1}
{γ : Type u_2}
[inst : CancelCommMonoidWithZero α]
[inst : NormalizedGCDMonoid α]
{f : β → α}
[inst : DecidableEq β]
{g : γ → β}
(s : Finset γ)
:
Finset.gcd (Finset.image g s) f = Finset.gcd s (f ∘ g)
theorem
Finset.gcd_eq_gcd_image
{α : Type u_1}
{β : Type u_2}
[inst : CancelCommMonoidWithZero α]
[inst : NormalizedGCDMonoid α]
{s : Finset β}
{f : β → α}
[inst : DecidableEq α]
:
Finset.gcd s f = Finset.gcd (Finset.image f s) id
theorem
Finset.gcd_eq_zero_iff
{α : Type u_1}
{β : Type u_2}
[inst : CancelCommMonoidWithZero α]
[inst : NormalizedGCDMonoid α]
{s : Finset β}
{f : β → α}
:
Finset.gcd s f = 0 ↔ ∀ (x : β), x ∈ s → f x = 0
theorem
Finset.gcd_eq_gcd_filter_ne_zero
{α : Type u_2}
{β : Type u_1}
[inst : CancelCommMonoidWithZero α]
[inst : NormalizedGCDMonoid α]
{s : Finset β}
{f : β → α}
[inst : 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_1}
{β : Type u_2}
[inst : CancelCommMonoidWithZero α]
[inst : 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_1}
{β : Type u_2}
[inst : CancelCommMonoidWithZero α]
[inst : 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_1}
[inst : CancelCommMonoidWithZero α]
[inst : NormalizedGCDMonoid α]
{s : Finset β}
(f : β → α)
(g : β → α)
(hs : ∃ x, x ∈ s ∧ f x ≠ 0)
(hg : ∀ (b : β), b ∈ s → f b = Finset.gcd s f * g b)
:
Finset.gcd s g = 1
theorem
Finset.extract_gcd
{α : Type u_2}
{β : Type u_1}
[inst : CancelCommMonoidWithZero α]
[inst : NormalizedGCDMonoid α]
{s : Finset β}
(f : β → α)
(hs : Finset.Nonempty s)
:
∃ g, (∀ (b : β), b ∈ s → f b = Finset.gcd s f * g b) ∧ Finset.gcd s g = 1
theorem
Finset.gcd_eq_of_dvd_sub
{α : Type u_2}
{β : Type u_1}
[inst : CommRing α]
[inst : IsDomain α]
[inst : NormalizedGCDMonoid α]
{s : Finset β}
{f : β → α}
{g : β → α}
{a : α}
(h : ∀ (x : β), x ∈ s → a ∣ f x - g x)
:
gcd a (Finset.gcd s f) = gcd a (Finset.gcd s g)