Documentation

Mathlib.Algebra.GCDMonoid.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} [inst : CancelCommMonoidWithZero α] [inst : NormalizedGCDMonoid α] (s : Finset β) (f : βα) :
α

Least common multiple of a finite set

Equations
theorem Finset.lcm_def {α : Type u_1} {β : Type u_2} [inst : CancelCommMonoidWithZero α] [inst : NormalizedGCDMonoid α] {s : Finset β} {f : βα} :
@[simp]
theorem Finset.lcm_empty {α : Type u_1} {β : Type u_2} [inst : CancelCommMonoidWithZero α] [inst : NormalizedGCDMonoid α] {f : βα} :
@[simp]
theorem Finset.lcm_dvd_iff {α : Type u_1} {β : Type u_2} [inst : CancelCommMonoidWithZero α] [inst : NormalizedGCDMonoid α] {s : Finset β} {f : βα} {a : α} :
Finset.lcm s f a ∀ (b : β), b sf b a
theorem Finset.lcm_dvd {α : Type u_2} {β : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : NormalizedGCDMonoid α] {s : Finset β} {f : βα} {a : α} :
(∀ (b : β), b sf b a) → Finset.lcm s f a
theorem Finset.dvd_lcm {α : Type u_2} {β : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : NormalizedGCDMonoid α] {s : Finset β} {f : βα} {b : β} (hb : b s) :
f b Finset.lcm s f
@[simp]
theorem Finset.lcm_insert {α : Type u_2} {β : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : NormalizedGCDMonoid α] {s : Finset β} {f : βα} [inst : 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} [inst : CancelCommMonoidWithZero α] [inst : NormalizedGCDMonoid α] {f : βα} {b : β} :
Finset.lcm {b} f = normalize (f b)
@[simp]
theorem Finset.normalize_lcm {α : Type u_1} {β : Type u_2} [inst : CancelCommMonoidWithZero α] [inst : NormalizedGCDMonoid α] {s : Finset β} {f : βα} :
normalize (Finset.lcm s f) = Finset.lcm s f
theorem Finset.lcm_union {α : Type u_2} {β : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : NormalizedGCDMonoid α] {s₁ : Finset β} {s₂ : Finset β} {f : βα} [inst : DecidableEq β] :
Finset.lcm (s₁ s₂) f = lcm (Finset.lcm s₁ f) (Finset.lcm s₂ f)
theorem Finset.lcm_congr {α : Type u_2} {β : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : 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_2} {β : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : NormalizedGCDMonoid α] {s : Finset β} {f : βα} {g : βα} (h : ∀ (b : β), b sf b g b) :
theorem Finset.lcm_mono {α : Type u_2} {β : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : NormalizedGCDMonoid α] {s₁ : Finset β} {s₂ : Finset β} {f : βα} (h : s₁ s₂) :
Finset.lcm s₁ f Finset.lcm s₂ f
theorem Finset.lcm_image {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : CancelCommMonoidWithZero α] [inst : NormalizedGCDMonoid α] {f : βα} [inst : DecidableEq β] {g : γβ} (s : Finset γ) :
theorem Finset.lcm_eq_lcm_image {α : Type u_1} {β : Type u_2} [inst : CancelCommMonoidWithZero α] [inst : NormalizedGCDMonoid α] {s : Finset β} {f : βα} [inst : DecidableEq α] :
theorem Finset.lcm_eq_zero_iff {α : Type u_1} {β : Type u_2} [inst : CancelCommMonoidWithZero α] [inst : NormalizedGCDMonoid α] {s : Finset β} {f : βα} [inst : Nontrivial α] :
Finset.lcm s f = 0 0 f '' s

gcd #

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

Greatest common divisor of a finite set

Equations
theorem Finset.gcd_def {α : Type u_1} {β : Type u_2} [inst : CancelCommMonoidWithZero α] [inst : NormalizedGCDMonoid α] {s : Finset β} {f : βα} :
@[simp]
theorem Finset.gcd_empty {α : Type u_1} {β : Type u_2} [inst : CancelCommMonoidWithZero α] [inst : NormalizedGCDMonoid α] {f : βα} :
theorem Finset.dvd_gcd_iff {α : Type u_1} {β : Type u_2} [inst : CancelCommMonoidWithZero α] [inst : NormalizedGCDMonoid α] {s : Finset β} {f : βα} {a : α} :
a Finset.gcd s f ∀ (b : β), b sa f b
theorem Finset.gcd_dvd {α : Type u_2} {β : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : NormalizedGCDMonoid α] {s : Finset β} {f : βα} {b : β} (hb : b s) :
Finset.gcd s f f b
theorem Finset.dvd_gcd {α : Type u_2} {β : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : NormalizedGCDMonoid α] {s : Finset β} {f : βα} {a : α} :
(∀ (b : β), b sa f b) → a Finset.gcd s f
@[simp]
theorem Finset.gcd_insert {α : Type u_2} {β : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : NormalizedGCDMonoid α] {s : Finset β} {f : βα} [inst : 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} [inst : CancelCommMonoidWithZero α] [inst : NormalizedGCDMonoid α] {f : βα} {b : β} :
Finset.gcd {b} f = normalize (f b)
@[simp]
theorem Finset.normalize_gcd {α : Type u_1} {β : Type u_2} [inst : CancelCommMonoidWithZero α] [inst : NormalizedGCDMonoid α] {s : Finset β} {f : βα} :
normalize (Finset.gcd s f) = Finset.gcd s f
theorem Finset.gcd_union {α : Type u_2} {β : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : NormalizedGCDMonoid α] {s₁ : Finset β} {s₂ : Finset β} {f : βα} [inst : DecidableEq β] :
Finset.gcd (s₁ s₂) f = gcd (Finset.gcd s₁ f) (Finset.gcd s₂ f)
theorem Finset.gcd_congr {α : Type u_2} {β : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : 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_2} {β : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : NormalizedGCDMonoid α] {s : Finset β} {f : βα} {g : βα} (h : ∀ (b : β), b sf b g b) :
theorem Finset.gcd_mono {α : Type u_2} {β : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : NormalizedGCDMonoid α] {s₁ : Finset β} {s₂ : Finset β} {f : βα} (h : s₁ s₂) :
Finset.gcd s₂ f Finset.gcd s₁ f
theorem Finset.gcd_image {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : CancelCommMonoidWithZero α] [inst : NormalizedGCDMonoid α] {f : βα} [inst : DecidableEq β] {g : γβ} (s : Finset γ) :
theorem Finset.gcd_eq_gcd_image {α : Type u_1} {β : Type u_2} [inst : CancelCommMonoidWithZero α] [inst : NormalizedGCDMonoid α] {s : Finset β} {f : βα} [inst : DecidableEq α] :
theorem Finset.gcd_eq_zero_iff {α : Type u_1} {β : Type u_2} [inst : CancelCommMonoidWithZero α] [inst : NormalizedGCDMonoid α] {s : Finset β} {f : βα} :
Finset.gcd s f = 0 ∀ (x : β), x sf x = 0
theorem Finset.gcd_eq_gcd_filter_ne_zero {α : Type u_2} {β : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : NormalizedGCDMonoid α] {s : Finset β} {f : βα} [inst : 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} [inst : CancelCommMonoidWithZero α] [inst : 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} [inst : CancelCommMonoidWithZero α] [inst : 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_2} {β : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : NormalizedGCDMonoid α] {s : Finset β} (f : βα) (g : βα) (hs : x, x s f x 0) (hg : ∀ (b : β), b sf b = Finset.gcd s f * g b) :
theorem Finset.extract_gcd {α : Type u_2} {β : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : NormalizedGCDMonoid α] {s : Finset β} (f : βα) (hs : Finset.Nonempty s) :
g, (∀ (b : β), b sf b = Finset.gcd s f * g b) Finset.gcd s g = 1
theorem Finset.gcd_eq_of_dvd_sub {α : Type u_2} {β : Type u_1} [inst : CommRing α] [inst : IsDomain α] [inst : NormalizedGCDMonoid α] {s : Finset β} {f : βα} {g : βα} {a : α} (h : ∀ (x : β), x sa f x - g x) :
gcd a (Finset.gcd s f) = gcd a (Finset.gcd s g)