mathlib documentation

data.finset.gcd

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

Least common multiple of a finite set

Equations
theorem finset.lcm_def {α : Type u_1} {β : Type u_2} [comm_cancel_monoid_with_zero α] [nontrivial α] [gcd_monoid α] {s : finset β} {f : β → α} :

@[simp]
theorem finset.lcm_empty {α : Type u_1} {β : Type u_2} [comm_cancel_monoid_with_zero α] [nontrivial α] [gcd_monoid α] {f : β → α} :
.lcm f = 1

@[simp]
theorem finset.lcm_dvd_iff {α : Type u_1} {β : Type u_2} [comm_cancel_monoid_with_zero α] [nontrivial α] [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} [comm_cancel_monoid_with_zero α] [nontrivial α] [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} [comm_cancel_monoid_with_zero α] [nontrivial α] [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} [comm_cancel_monoid_with_zero α] [nontrivial α] [gcd_monoid α] {s : finset β} {f : β → α} [decidable_eq β] {b : β} :
(insert b s).lcm f = lcm (f b) (s.lcm f)

@[simp]
theorem finset.lcm_singleton {α : Type u_1} {β : Type u_2} [comm_cancel_monoid_with_zero α] [nontrivial α] [gcd_monoid α] {f : β → α} {b : β} :
{b}.lcm f = normalize (f b)

@[simp]
theorem finset.normalize_lcm {α : Type u_1} {β : Type u_2} [comm_cancel_monoid_with_zero α] [nontrivial α] [gcd_monoid α] {s : finset β} {f : β → α} :
normalize (s.lcm f) = s.lcm f

theorem finset.lcm_union {α : Type u_1} {β : Type u_2} [comm_cancel_monoid_with_zero α] [nontrivial α] [gcd_monoid α] {s₁ s₂ : finset β} {f : β → α} [decidable_eq β] :
(s₁ s₂).lcm f = lcm (s₁.lcm f) (s₂.lcm f)

theorem finset.lcm_congr {α : Type u_1} {β : Type u_2} [comm_cancel_monoid_with_zero α] [nontrivial α] [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} [comm_cancel_monoid_with_zero α] [nontrivial α] [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} [comm_cancel_monoid_with_zero α] [nontrivial α] [gcd_monoid α] {s₁ s₂ : finset β} {f : β → α} (h : s₁ s₂) :
s₁.lcm f s₂.lcm f

gcd

def finset.gcd {α : Type u_1} {β : Type u_2} [comm_cancel_monoid_with_zero α] [nontrivial α] [gcd_monoid α] (s : finset β) (f : β → α) :
α

Greatest common divisor of a finite set

Equations
theorem finset.gcd_def {α : Type u_1} {β : Type u_2} [comm_cancel_monoid_with_zero α] [nontrivial α] [gcd_monoid α] {s : finset β} {f : β → α} :

@[simp]
theorem finset.gcd_empty {α : Type u_1} {β : Type u_2} [comm_cancel_monoid_with_zero α] [nontrivial α] [gcd_monoid α] {f : β → α} :
.gcd f = 0

theorem finset.dvd_gcd_iff {α : Type u_1} {β : Type u_2} [comm_cancel_monoid_with_zero α] [nontrivial α] [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} [comm_cancel_monoid_with_zero α] [nontrivial α] [gcd_monoid α] {s : finset β} {f : β → α} {b : β} (hb : b s) :
s.gcd f f b

theorem finset.dvd_gcd {α : Type u_1} {β : Type u_2} [comm_cancel_monoid_with_zero α] [nontrivial α] [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} [comm_cancel_monoid_with_zero α] [nontrivial α] [gcd_monoid α] {s : finset β} {f : β → α} [decidable_eq β] {b : β} :
(insert b s).gcd f = gcd (f b) (s.gcd f)

@[simp]
theorem finset.gcd_singleton {α : Type u_1} {β : Type u_2} [comm_cancel_monoid_with_zero α] [nontrivial α] [gcd_monoid α] {f : β → α} {b : β} :
{b}.gcd f = normalize (f b)

@[simp]
theorem finset.normalize_gcd {α : Type u_1} {β : Type u_2} [comm_cancel_monoid_with_zero α] [nontrivial α] [gcd_monoid α] {s : finset β} {f : β → α} :
normalize (s.gcd f) = s.gcd f

theorem finset.gcd_union {α : Type u_1} {β : Type u_2} [comm_cancel_monoid_with_zero α] [nontrivial α] [gcd_monoid α] {s₁ s₂ : finset β} {f : β → α} [decidable_eq β] :
(s₁ s₂).gcd f = gcd (s₁.gcd f) (s₂.gcd f)

theorem finset.gcd_congr {α : Type u_1} {β : Type u_2} [comm_cancel_monoid_with_zero α] [nontrivial α] [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} [comm_cancel_monoid_with_zero α] [nontrivial α] [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} [comm_cancel_monoid_with_zero α] [nontrivial α] [gcd_monoid α] {s₁ s₂ : finset β} {f : β → α} (h : s₁ s₂) :
s₂.gcd f s₁.gcd f

theorem finset.gcd_eq_zero_iff {α : Type u_1} {β : Type u_2} [comm_cancel_monoid_with_zero α] [nontrivial α] [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} [comm_cancel_monoid_with_zero α] [nontrivial α] [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} [comm_cancel_monoid_with_zero α] [nontrivial α] [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} [comm_cancel_monoid_with_zero α] [nontrivial α] [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} [nontrivial β] [integral_domain α] [gcd_monoid α] {s : finset β} {f g : β → α} {a : α} (h : ∀ (x : β), x sa f x - g x) :
gcd a (s.gcd f) = gcd a (s.gcd g)