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_1} {β : Type u_2} [CancelCommMonoidWithZero α] [NormalizedGCDMonoid α] (s : Finset β) (f : β → α) : α

Least common multiple of a finite set

theorem Finset.lcm_def {α : Type u_1} {β : Type u_2} [CancelCommMonoidWithZero α] [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} [CancelCommMonoidWithZero α] [NormalizedGCDMonoid α] {f : β → α} : Finset.lcm ∅ f = 1

@[simp]

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

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

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

@[simp]

theorem Finset.lcm_insert {α : Type u_1} {β : Type u_2} [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_1} {β : Type u_2} [CancelCommMonoidWithZero α] [NormalizedGCDMonoid α] {f : β → α} {b : β} : Finset.lcm {b} f = ↑normalize (f b)

@[simp]

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

theorem Finset.lcm_union {α : Type u_1} {β : Type u_2} [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_1} {β : Type u_2} [CancelCommMonoidWithZero α] [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_1} {β : Type u_2} [CancelCommMonoidWithZero α] [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_1} {β : Type u_2} [CancelCommMonoidWithZero α] [NormalizedGCDMonoid α] {s₁ : Finset β} {s₂ : Finset β} {f : β → α} (h : s₁ ⊆ s₂) : Finset.lcm s₁ f ∣ Finset.lcm s₂ f

theorem Finset.lcm_image {α : Type u_1} {β : Type u_2} {γ : Type u_3} [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_1} {β : Type u_2} [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_1} {β : Type u_2} [CancelCommMonoidWithZero α] [NormalizedGCDMonoid α] {s : Finset β} {f : β → α} [Nontrivial α] : Finset.lcm s f = 0 ↔ 0 ∈ f '' ↑s

gcd

def Finset.gcd {α : Type u_1} {β : Type u_2} [CancelCommMonoidWithZero α] [NormalizedGCDMonoid α] (s : Finset β) (f : β → α) : α

Greatest common divisor of a finite set

theorem Finset.gcd_def {α : Type u_1} {β : Type u_2} [CancelCommMonoidWithZero α] [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} [CancelCommMonoidWithZero α] [NormalizedGCDMonoid α] {f : β → α} : Finset.gcd ∅ f = 0

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

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

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

@[simp]

theorem Finset.gcd_insert {α : Type u_1} {β : Type u_2} [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_1} {β : Type u_2} [CancelCommMonoidWithZero α] [NormalizedGCDMonoid α] {f : β → α} {b : β} : Finset.gcd {b} f = ↑normalize (f b)

@[simp]

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

theorem Finset.gcd_union {α : Type u_1} {β : Type u_2} [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_1} {β : Type u_2} [CancelCommMonoidWithZero α] [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_1} {β : Type u_2} [CancelCommMonoidWithZero α] [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_1} {β : Type u_2} [CancelCommMonoidWithZero α] [NormalizedGCDMonoid α] {s₁ : Finset β} {s₂ : Finset β} {f : β → α} (h : s₁ ⊆ s₂) : Finset.gcd s₂ f ∣ Finset.gcd s₁ f

theorem Finset.gcd_image {α : Type u_1} {β : Type u_2} {γ : Type u_3} [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_1} {β : Type u_2} [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_1} {β : Type u_2} [CancelCommMonoidWithZero α] [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_1} {β : Type u_2} [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_1} {β : Type u_2} [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_1} {β : Type u_2} [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_1} {β : Type u_2} [CancelCommMonoidWithZero α] [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_1} {β : Type u_2} [CancelCommMonoidWithZero α] [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_1} {β : Type u_2} [CommRing α] [IsDomain α] [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)