mathlib3 documentation

algebra.gcd_monoid.finset

GCD and LCM operations on finsets #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 s f 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 s f 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 s f 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 s a 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 s a 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 s f 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 s f 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.extract_gcd' {α : Type u_1} {β : Type u_2} [cancel_comm_monoid_with_zero α] [normalized_gcd_monoid α] {s : finset β} (f g : β α) (hs : (x : β), x s f x 0) (hg : (b : β), b s f b = s.gcd f * g b) :
s.gcd g = 1
theorem finset.extract_gcd {α : Type u_1} {β : Type u_2} [cancel_comm_monoid_with_zero α] [normalized_gcd_monoid α] {s : finset β} (f : β α) (hs : s.nonempty) :
(g : β α), ( (b : β), b s f b = s.gcd f * g b) s.gcd g = 1
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) :