GCD and LCM operations on finsets

Main definitions

• Finset.gcd - the greatest common denominator of a Finset of elements of a GCDMonoid
• Finset.lcm - the least common multiple of a Finset of elements of a GCDMonoid

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} [CommMonoidWithZero α] [NormalizedGCDMonoid α] (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_2} {β : Type u_3} [CommMonoidWithZero α] [NormalizedGCDMonoid α] {s : Finset β} {f : β → α} : s.lcm f = (Multiset.map f s.val).lcm

@[simp]

theorem Finset.lcm_empty {α : Type u_2} {β : Type u_3} [CommMonoidWithZero α] [NormalizedGCDMonoid α] {f : β → α} : ∅.lcm f = 1

@[simp]

theorem Finset.lcm_dvd_iff {α : Type u_2} {β : Type u_3} [CommMonoidWithZero α] [NormalizedGCDMonoid α] {s : Finset β} {f : β → α} {a : α} : s.lcm f ∣ a ↔ ∀ b ∈ s, f b ∣ a

theorem Finset.lcm_dvd {α : Type u_2} {β : Type u_3} [CommMonoidWithZero α] [NormalizedGCDMonoid α] {s : Finset β} {f : β → α} {a : α} : (∀ b ∈ s, f b ∣ a) → s.lcm f ∣ a

theorem Finset.dvd_lcm {α : Type u_2} {β : Type u_3} [CommMonoidWithZero α] [NormalizedGCDMonoid α] {s : Finset β} {f : β → α} {b : β} (hb : b ∈ s) : f b ∣ s.lcm f

@[simp]

theorem Finset.lcm_insert {α : Type u_2} {β : Type u_3} [CommMonoidWithZero α] [NormalizedGCDMonoid α] {s : Finset β} {f : β → α} [DecidableEq β] {b : β} : (insert b s).lcm f = GCDMonoid.lcm (f b) (s.lcm f)

@[simp]

theorem Finset.lcm_singleton {α : Type u_2} {β : Type u_3} [CommMonoidWithZero α] [NormalizedGCDMonoid α] {f : β → α} {b : β} : {b}.lcm f = normalize (f b)

theorem Finset.normalize_lcm {α : Type u_2} {β : Type u_3} [CommMonoidWithZero α] [NormalizedGCDMonoid α] {s : Finset β} {f : β → α} : normalize (s.lcm f) = s.lcm f

theorem Finset.lcm_union {α : Type u_2} {β : Type u_3} [CommMonoidWithZero α] [NormalizedGCDMonoid α] {s₁ s₂ : Finset β} {f : β → α} [DecidableEq β] : (s₁ ∪ s₂).lcm f = GCDMonoid.lcm (s₁.lcm f) (s₂.lcm f)

theorem Finset.lcm_congr {α : Type u_2} {β : Type u_3} [CommMonoidWithZero α] [NormalizedGCDMonoid α] {s₁ s₂ : Finset β} {f g : β → α} (hs : s₁ = s₂) (hfg : ∀ a ∈ s₂, f a = g a) : s₁.lcm f = s₂.lcm g

theorem Finset.lcm_mono_fun {α : Type u_2} {β : Type u_3} [CommMonoidWithZero α] [NormalizedGCDMonoid α] {s : Finset β} {f g : β → α} (h : ∀ b ∈ s, f b ∣ g b) : s.lcm f ∣ s.lcm g

theorem Finset.lcm_mono {α : Type u_2} {β : Type u_3} [CommMonoidWithZero α] [NormalizedGCDMonoid α] {s₁ s₂ : Finset β} {f : β → α} (h : s₁ ⊆ s₂) : s₁.lcm f ∣ s₂.lcm f

theorem Finset.lcm_image {α : Type u_2} {β : Type u_3} {γ : Type u_4} [CommMonoidWithZero α] [NormalizedGCDMonoid α] {f : β → α} [DecidableEq β] {g : γ → β} (s : Finset γ) : (image g s).lcm f = s.lcm (f ∘ g)

theorem Finset.lcm_eq_lcm_image {α : Type u_2} {β : Type u_3} [CommMonoidWithZero α] [NormalizedGCDMonoid α] {s : Finset β} {f : β → α} [DecidableEq α] : s.lcm f = (image f s).lcm id

@[simp]

theorem Finset.lcm_eq_zero_iff {α : Type u_2} {β : Type u_3} [CommMonoidWithZero α] [NormalizedGCDMonoid α] {s : Finset β} {f : β → α} [Nontrivial α] : s.lcm f = 0 ↔ ∃ x ∈ s, f x = 0

theorem Finset.lcm_ne_zero_iff {α : Type u_2} {β : Type u_3} [CommMonoidWithZero α] [NormalizedGCDMonoid α] {s : Finset β} {f : β → α} [Nontrivial α] : s.lcm f ≠ 0 ↔ ∀ x ∈ s, f x ≠ 0

gcd

def Finset.gcd {α : Type u_2} {β : Type u_3} [CommMonoidWithZero α] [NormalizedGCDMonoid α] (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_2} {β : Type u_3} [CommMonoidWithZero α] [NormalizedGCDMonoid α] {s : Finset β} {f : β → α} : s.gcd f = (Multiset.map f s.val).gcd

@[simp]

theorem Finset.gcd_empty {α : Type u_2} {β : Type u_3} [CommMonoidWithZero α] [NormalizedGCDMonoid α] {f : β → α} : ∅.gcd f = 0

theorem Finset.dvd_gcd_iff {α : Type u_2} {β : Type u_3} [CommMonoidWithZero α] [NormalizedGCDMonoid α] {s : Finset β} {f : β → α} {a : α} : a ∣ s.gcd f ↔ ∀ b ∈ s, a ∣ f b

theorem Finset.gcd_dvd {α : Type u_2} {β : Type u_3} [CommMonoidWithZero α] [NormalizedGCDMonoid α] {s : Finset β} {f : β → α} {b : β} (hb : b ∈ s) : s.gcd f ∣ f b

theorem Finset.dvd_gcd {α : Type u_2} {β : Type u_3} [CommMonoidWithZero α] [NormalizedGCDMonoid α] {s : Finset β} {f : β → α} {a : α} : (∀ b ∈ s, a ∣ f b) → a ∣ s.gcd f

theorem Finset.gcd_cons {α : Type u_2} {β : Type u_3} [CommMonoidWithZero α] [NormalizedGCDMonoid α] {s : Finset β} {f : β → α} {b : β} (h : b ∉ s) : (cons b s h).gcd f = GCDMonoid.gcd (f b) (s.gcd f)

@[simp]

theorem Finset.gcd_insert {α : Type u_2} {β : Type u_3} [CommMonoidWithZero α] [NormalizedGCDMonoid α] {s : Finset β} {f : β → α} [DecidableEq β] {b : β} : (insert b s).gcd f = GCDMonoid.gcd (f b) (s.gcd f)

@[simp]

theorem Finset.gcd_singleton {α : Type u_2} {β : Type u_3} [CommMonoidWithZero α] [NormalizedGCDMonoid α] {f : β → α} {b : β} : {b}.gcd f = normalize (f b)

theorem Finset.normalize_gcd {α : Type u_2} {β : Type u_3} [CommMonoidWithZero α] [NormalizedGCDMonoid α] {s : Finset β} {f : β → α} : normalize (s.gcd f) = s.gcd f

theorem Finset.gcd_union {α : Type u_2} {β : Type u_3} [CommMonoidWithZero α] [NormalizedGCDMonoid α] {s₁ s₂ : Finset β} {f : β → α} [DecidableEq β] : (s₁ ∪ s₂).gcd f = GCDMonoid.gcd (s₁.gcd f) (s₂.gcd f)

theorem Finset.gcd_congr {α : Type u_2} {β : Type u_3} [CommMonoidWithZero α] [NormalizedGCDMonoid α] {s₁ s₂ : Finset β} {f g : β → α} (hs : s₁ = s₂) (hfg : ∀ a ∈ s₂, f a = g a) : s₁.gcd f = s₂.gcd g

theorem Finset.gcd_mono_fun {α : Type u_2} {β : Type u_3} [CommMonoidWithZero α] [NormalizedGCDMonoid α] {s : Finset β} {f g : β → α} (h : ∀ b ∈ s, f b ∣ g b) : s.gcd f ∣ s.gcd g

theorem Finset.gcd_mono {α : Type u_2} {β : Type u_3} [CommMonoidWithZero α] [NormalizedGCDMonoid α] {s₁ s₂ : Finset β} {f : β → α} (h : s₁ ⊆ s₂) : s₂.gcd f ∣ s₁.gcd f

theorem Finset.gcd_image {α : Type u_2} {β : Type u_3} {γ : Type u_4} [CommMonoidWithZero α] [NormalizedGCDMonoid α] {f : β → α} [DecidableEq β] {g : γ → β} (s : Finset γ) : (image g s).gcd f = s.gcd (f ∘ g)

theorem Finset.gcd_eq_gcd_image {α : Type u_2} {β : Type u_3} [CommMonoidWithZero α] [NormalizedGCDMonoid α] {s : Finset β} {f : β → α} [DecidableEq α] : s.gcd f = (image f s).gcd id

theorem Finset.gcd_eq_zero_iff {α : Type u_2} {β : Type u_3} [CommMonoidWithZero α] [NormalizedGCDMonoid α] {s : Finset β} {f : β → α} : s.gcd f = 0 ↔ ∀ x ∈ s, f x = 0

theorem Finset.gcd_ne_zero_iff {α : Type u_2} {β : Type u_3} [CommMonoidWithZero α] [NormalizedGCDMonoid α] {s : Finset β} {f : β → α} : s.gcd f ≠ 0 ↔ ∃ x ∈ s, f x ≠ 0

theorem Finset.gcd_eq_gcd_filter_ne_zero {α : Type u_2} {β : Type u_3} [CommMonoidWithZero α] [NormalizedGCDMonoid α] {s : Finset β} {f : β → α} [DecidablePred fun (x : β) => f x = 0] : s.gcd f = {x ∈ s | f x ≠ 0}.gcd f

theorem Finset.gcd_mul_left {β : Type u_3} {α : Type u_5} [CommMonoidWithZero α] [StrongNormalizedGCDMonoid α] {s : Finset β} {f : β → α} {a : α} : (s.gcd fun (x : β) => a * f x) = normalize a * s.gcd f

theorem Finset.gcd_mul_right {β : Type u_3} {α : Type u_5} [CommMonoidWithZero α] [StrongNormalizedGCDMonoid α] {s : Finset β} {f : β → α} {a : α} : (s.gcd fun (x : β) => f x * a) = s.gcd f * normalize a

theorem Finset.gcd_mul_left' {α : Type u_2} {β : Type u_3} [CommMonoidWithZero α] [NormalizedGCDMonoid α] (s : Finset β) (f : β → α) (a : α) : Associated (s.gcd fun (x : β) => a * f x) (a * s.gcd f)

theorem Finset.gcd_mul_right' {α : Type u_2} {β : Type u_3} [CommMonoidWithZero α] [NormalizedGCDMonoid α] (s : Finset β) (f : β → α) (a : α) : Associated (s.gcd fun (x : β) => f x * a) (s.gcd f * a)

theorem Finset.extract_gcd' {α : Type u_2} {β : Type u_3} [CommMonoidWithZero α] [NormalizedGCDMonoid α] {s : Finset β} (f g : β → α) (hs : ∃ x ∈ s, f x ≠ 0) (hg : ∀ b ∈ s, f b = s.gcd f * g b) : s.gcd g = 1

theorem Finset.extract_gcd {α : Type u_2} {β : Type u_3} [CommMonoidWithZero α] [NormalizedGCDMonoid α] {s : Finset β} (f : β → α) (hs : s.Nonempty) : ∃ (g : β → α), (∀ b ∈ s, f b = s.gcd f * g b) ∧ s.gcd g = 1

theorem Finset.gcd_div_eq_one {ι : Type u_1} {α : Type u_2} [CommMonoidWithZero α] [NormalizedGCDMonoid α] [Div α] [MulDivCancelClass α] {f : ι → α} {s : Finset ι} {i : ι} (his : i ∈ s) (hfi : f i ≠ 0) : (s.gcd fun (j : ι) => f j / s.gcd 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} [CommMonoidWithZero α] [NormalizedGCDMonoid α] [Div α] [MulDivCancelClass α] {s : Finset α} {a : α} (has : a ∈ s) (ha : a ≠ 0) : (s.gcd fun (b : α) => b / s.gcd id) = 1

theorem Finset.gcd_eq_of_dvd_sub {α : Type u_2} {β : Type u_3} [CommRing α] [NormalizedGCDMonoid α] {s : Finset β} {f g : β → α} {a : α} (h : ∀ x ∈ s, a ∣ f x - g x) : GCDMonoid.gcd a (s.gcd f) = GCDMonoid.gcd a (s.gcd g)

theorem Finset.Int.finsetGcd_nonneg {ι : Type u_1} {s : Finset ι} {f : ι → ℤ} : 0 ≤ s.gcd f

The gcd of a finset of integers is nonnegative.