GCD and LCM operations on finsets #

Main definitions #

finset.gcd - the greatest common denominator of a finset of elements of a gcd_monoid
finset.lcm - the least common multiple of a finset of elements of a gcd_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 #

source

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 lcm 1 f s

source

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

source

@[simp]

theorem finset.lcm_empty {α : Type u_1} {β : Type u_2} [cancel_comm_monoid_with_zero α] [normalized_gcd_monoid α] {f : β → α} :

∅.lcm f = 1

source

@[simp]

theorem finset.lcm_dvd_iff {α : Type u_1} {β : Type u_2} [cancel_comm_monoid_with_zero α] [normalized_gcd_monoid α] {s : finset β} {f : β → α} {a : α} :

s.lcm f ∣ a ↔ ∀ (b : β), b ∈ s → f b ∣ a

source

theorem finset.lcm_dvd {α : Type u_1} {β : Type u_2} [cancel_comm_monoid_with_zero α] [normalized_gcd_monoid α] {s : finset β} {f : β → α} {a : α} :

(∀ (b : β), b ∈ s → f b ∣ a) → s.lcm f ∣ a

source

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) :

f b ∣ s.lcm f

source

@[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 : β} :

(insert b s).lcm f = lcm (f b) (s.lcm f)

source

@[simp]

theorem finset.lcm_singleton {α : Type u_1} {β : Type u_2} [cancel_comm_monoid_with_zero α] [normalized_gcd_monoid α] {f : β → α} {b : β} :

{b}.lcm f = ⇑normalize (f b)

source

@[simp]

theorem finset.normalize_lcm {α : Type u_1} {β : Type u_2} [cancel_comm_monoid_with_zero α] [normalized_gcd_monoid α] {s : finset β} {f : β → α} :

⇑normalize (s.lcm f) = s.lcm f

source

theorem finset.lcm_union {α : Type u_1} {β : Type u_2} [cancel_comm_monoid_with_zero α] [normalized_gcd_monoid α] {s₁ s₂ : finset β} {f : β → α} [decidable_eq β] :

(s₁ ∪ s₂).lcm f = lcm (s₁.lcm f) (s₂.lcm f)

source

theorem finset.lcm_congr {α : Type u_1} {β : Type u_2} [cancel_comm_monoid_with_zero α] [normalized_gcd_monoid α] {s₁ s₂ : finset β} {f g : β → α} (hs : s₁ = s₂) (hfg : ∀ (a : β), a ∈ s₂ → f a = g a) :

s₁.lcm f = s₂.lcm g

source

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) :

s.lcm f ∣ s.lcm g

source

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₂) :

s₁.lcm f ∣ s₂.lcm f

source

theorem finset.lcm_eq_zero_iff {α : Type u_1} {β : Type u_2} [cancel_comm_monoid_with_zero α] [normalized_gcd_monoid α] {s : finset β} {f : β → α} [nontrivial α] :

s.lcm f = 0 ↔ 0 ∈ f '' ↑s

gcd #

source

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 0 f s

source

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

source

@[simp]

theorem finset.gcd_empty {α : Type u_1} {β : Type u_2} [cancel_comm_monoid_with_zero α] [normalized_gcd_monoid α] {f : β → α} :

∅.gcd f = 0

source

theorem finset.dvd_gcd_iff {α : Type u_1} {β : Type u_2} [cancel_comm_monoid_with_zero α] [normalized_gcd_monoid α] {s : finset β} {f : β → α} {a : α} :

a ∣ s.gcd f ↔ ∀ (b : β), b ∈ s → a ∣ f b

source

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) :

s.gcd f ∣ f b

source

theorem finset.dvd_gcd {α : Type u_1} {β : Type u_2} [cancel_comm_monoid_with_zero α] [normalized_gcd_monoid α] {s : finset β} {f : β → α} {a : α} :

(∀ (b : β), b ∈ s → a ∣ f b) → a ∣ s.gcd f

source

@[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 : β} :

(insert b s).gcd f = gcd (f b) (s.gcd f)

source

@[simp]

theorem finset.gcd_singleton {α : Type u_1} {β : Type u_2} [cancel_comm_monoid_with_zero α] [normalized_gcd_monoid α] {f : β → α} {b : β} :

{b}.gcd f = ⇑normalize (f b)

source

@[simp]

theorem finset.normalize_gcd {α : Type u_1} {β : Type u_2} [cancel_comm_monoid_with_zero α] [normalized_gcd_monoid α] {s : finset β} {f : β → α} :

⇑normalize (s.gcd f) = s.gcd f

source

theorem finset.gcd_union {α : Type u_1} {β : Type u_2} [cancel_comm_monoid_with_zero α] [normalized_gcd_monoid α] {s₁ s₂ : finset β} {f : β → α} [decidable_eq β] :

(s₁ ∪ s₂).gcd f = gcd (s₁.gcd f) (s₂.gcd f)

source

theorem finset.gcd_congr {α : Type u_1} {β : Type u_2} [cancel_comm_monoid_with_zero α] [normalized_gcd_monoid α] {s₁ s₂ : finset β} {f g : β → α} (hs : s₁ = s₂) (hfg : ∀ (a : β), a ∈ s₂ → f a = g a) :

s₁.gcd f = s₂.gcd g

source

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) :

s.gcd f ∣ s.gcd g

source

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₂) :

s₂.gcd f ∣ s₁.gcd f

source

theorem finset.gcd_image {α : Type u_1} {β : Type u_2} {γ : Type u_3} [cancel_comm_monoid_with_zero α] [normalized_gcd_monoid α] {f : β → α} {g : γ → β} (s : finset γ) [decidable_eq β] [is_idempotent α gcd] :

(finset.image g s).gcd f = s.gcd (f ∘ g)

source

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 α] [is_idempotent α gcd] :

s.gcd f = (finset.image f s).gcd id

source

theorem finset.gcd_eq_zero_iff {α : Type u_1} {β : Type u_2} [cancel_comm_monoid_with_zero α] [normalized_gcd_monoid α] {s : finset β} {f : β → α} :

s.gcd f = 0 ↔ ∀ (x : β), x ∈ s → f x = 0

source

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

source

theorem finset.gcd_mul_left {α : Type u_1} {β : Type u_2} [cancel_comm_monoid_with_zero α] [normalized_gcd_monoid α] {s : finset β} {f : β → α} {a : α} :

s.gcd (λ (x : β), a * f x) = (⇑normalize a) * s.gcd f

source

theorem finset.gcd_mul_right {α : Type u_1} {β : Type u_2} [cancel_comm_monoid_with_zero α] [normalized_gcd_monoid α] {s : finset β} {f : β → α} {a : α} :

s.gcd (λ (x : β), (f x) * a) = (s.gcd f) * ⇑normalize a

source

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 a (s.gcd f) = gcd a (s.gcd g)