mathlib documentation

algebra.gcd_monoid.finset

GCD and LCM operations on finsets #

Main definitions #

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} [cancel_comm_monoid_with_zero α] [normalized_gcd_monoid α] (s : finset β) (f : β → α) :
α

Least common multiple of a finite set

Equations
theorem finset.lcm_def {α : Type u_1} {β : Type u_2} [cancel_comm_monoid_with_zero α] [normalized_gcd_monoid α] {s : finset β} {f : β → α} :
@[simp]
theorem finset.lcm_empty {α : Type u_1} {β : Type u_2} [cancel_comm_monoid_with_zero α] [normalized_gcd_monoid α] {f : β → α} :
.lcm f = 1
@[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 sf b a
theorem finset.lcm_dvd {α : Type u_1} {β : Type u_2} [cancel_comm_monoid_with_zero α] [normalized_gcd_monoid α] {s : finset β} {f : β → α} {a : α} :
(∀ (b : β), b sf b a)s.lcm f a
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
@[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 : β} :
@[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)
@[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
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 = gcd_monoid.lcm (s₁.lcm f) (s₂.lcm f)
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
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 sf b g b) :
s.lcm f s.lcm g
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
theorem finset.lcm_image {α : Type u_1} {β : Type u_2} {γ : Type u_3} [cancel_comm_monoid_with_zero α] [normalized_gcd_monoid α] {f : β → α} [decidable_eq β] {g : γ → β} (s : finset γ) :
(finset.image g s).lcm f = s.lcm (f g)
theorem finset.lcm_eq_lcm_image {α : Type u_1} {β : Type u_2} [cancel_comm_monoid_with_zero α] [normalized_gcd_monoid α] {s : finset β} {f : β → α} [decidable_eq α] :
s.lcm f = (finset.image f s).lcm id
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 #

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
theorem finset.gcd_def {α : Type u_1} {β : Type u_2} [cancel_comm_monoid_with_zero α] [normalized_gcd_monoid α] {s : finset β} {f : β → α} :
@[simp]
theorem finset.gcd_empty {α : Type u_1} {β : Type u_2} [cancel_comm_monoid_with_zero α] [normalized_gcd_monoid α] {f : β → α} :
.gcd f = 0
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 sa f b
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
theorem finset.dvd_gcd {α : Type u_1} {β : Type u_2} [cancel_comm_monoid_with_zero α] [normalized_gcd_monoid α] {s : finset β} {f : β → α} {a : α} :
(∀ (b : β), b sa f b)a s.gcd f
@[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 : β} :
@[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)
@[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
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_monoid.gcd (s₁.gcd f) (s₂.gcd f)
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
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 sf b g b) :
s.gcd f s.gcd g
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
theorem finset.gcd_image {α : Type u_1} {β : Type u_2} {γ : Type u_3} [cancel_comm_monoid_with_zero α] [normalized_gcd_monoid α] {f : β → α} [decidable_eq β] {g : γ → β} (s : finset γ) :
(finset.image g s).gcd f = s.gcd (f g)
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 α] :
s.gcd f = (finset.image f s).gcd id
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 sf x = 0
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
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
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
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 sa f x - g x) :