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_2} {β : Type u_3} [CancelCommMonoidWithZero α] [NormalizedGCDMonoid α] (s : Finset β) (f : βα) :
α

Least common multiple of a finite set

Equations
Instances For
    theorem Finset.lcm_def {α : Type u_2} {β : Type u_3} [CancelCommMonoidWithZero α] [NormalizedGCDMonoid α] {s : Finset β} {f : βα} :
    s.lcm f = (Multiset.map f s.val).lcm
    @[simp]
    theorem Finset.lcm_empty {α : Type u_2} {β : Type u_3} [CancelCommMonoidWithZero α] [NormalizedGCDMonoid α] {f : βα} :
    .lcm f = 1
    @[simp]
    theorem Finset.lcm_dvd_iff {α : Type u_2} {β : Type u_3} [CancelCommMonoidWithZero α] [NormalizedGCDMonoid α] {s : Finset β} {f : βα} {a : α} :
    s.lcm f a bs, f b a
    theorem Finset.lcm_dvd {α : Type u_2} {β : Type u_3} [CancelCommMonoidWithZero α] [NormalizedGCDMonoid α] {s : Finset β} {f : βα} {a : α} :
    (∀ bs, f b a)s.lcm f a
    theorem Finset.dvd_lcm {α : Type u_2} {β : Type u_3} [CancelCommMonoidWithZero α] [NormalizedGCDMonoid α] {s : Finset β} {f : βα} {b : β} (hb : b s) :
    f b s.lcm f
    @[simp]
    theorem Finset.lcm_insert {α : Type u_2} {β : Type u_3} [CancelCommMonoidWithZero α] [NormalizedGCDMonoid α] {s : Finset β} {f : βα} [DecidableEq β] {b : β} :
    (insert b s).lcm f = lcm (f b) (s.lcm f)
    @[simp]
    theorem Finset.lcm_singleton {α : Type u_2} {β : Type u_3} [CancelCommMonoidWithZero α] [NormalizedGCDMonoid α] {f : βα} {b : β} :
    {b}.lcm f = normalize (f b)
    @[simp]
    theorem Finset.normalize_lcm {α : Type u_2} {β : Type u_3} [CancelCommMonoidWithZero α] [NormalizedGCDMonoid α] {s : Finset β} {f : βα} :
    normalize (s.lcm f) = s.lcm f
    theorem Finset.lcm_union {α : Type u_2} {β : Type u_3} [CancelCommMonoidWithZero α] [NormalizedGCDMonoid α] {s₁ : Finset β} {s₂ : Finset β} {f : βα} [DecidableEq β] :
    (s₁ s₂).lcm f = lcm (s₁.lcm f) (s₂.lcm f)
    theorem Finset.lcm_congr {α : Type u_2} {β : Type u_3} [CancelCommMonoidWithZero α] [NormalizedGCDMonoid α] {s₁ : Finset β} {s₂ : Finset β} {f : βα} {g : βα} (hs : s₁ = s₂) (hfg : as₂, f a = g a) :
    s₁.lcm f = s₂.lcm g
    theorem Finset.lcm_mono_fun {α : Type u_2} {β : Type u_3} [CancelCommMonoidWithZero α] [NormalizedGCDMonoid α] {s : Finset β} {f : βα} {g : βα} (h : bs, f b g b) :
    s.lcm f s.lcm g
    theorem Finset.lcm_mono {α : Type u_2} {β : Type u_3} [CancelCommMonoidWithZero α] [NormalizedGCDMonoid α] {s₁ : Finset β} {s₂ : Finset β} {f : βα} (h : s₁ s₂) :
    s₁.lcm f s₂.lcm f
    theorem Finset.lcm_image {α : Type u_2} {β : Type u_3} {γ : Type u_4} [CancelCommMonoidWithZero α] [NormalizedGCDMonoid α] {f : βα} [DecidableEq β] {g : γβ} (s : Finset γ) :
    (Finset.image g s).lcm f = s.lcm (f g)
    theorem Finset.lcm_eq_lcm_image {α : Type u_2} {β : Type u_3} [CancelCommMonoidWithZero α] [NormalizedGCDMonoid α] {s : Finset β} {f : βα} [DecidableEq α] :
    s.lcm f = (Finset.image f s).lcm id
    theorem Finset.lcm_eq_zero_iff {α : Type u_2} {β : Type u_3} [CancelCommMonoidWithZero α] [NormalizedGCDMonoid α] {s : Finset β} {f : βα} [Nontrivial α] :
    s.lcm f = 0 0 f '' s

    gcd #

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

    Greatest common divisor of a finite set

    Equations
    Instances For
      theorem Finset.gcd_def {α : Type u_2} {β : Type u_3} [CancelCommMonoidWithZero α] [NormalizedGCDMonoid α] {s : Finset β} {f : βα} :
      s.gcd f = (Multiset.map f s.val).gcd
      @[simp]
      theorem Finset.gcd_empty {α : Type u_2} {β : Type u_3} [CancelCommMonoidWithZero α] [NormalizedGCDMonoid α] {f : βα} :
      .gcd f = 0
      theorem Finset.dvd_gcd_iff {α : Type u_2} {β : Type u_3} [CancelCommMonoidWithZero α] [NormalizedGCDMonoid α] {s : Finset β} {f : βα} {a : α} :
      a s.gcd f bs, a f b
      theorem Finset.gcd_dvd {α : Type u_2} {β : Type u_3} [CancelCommMonoidWithZero α] [NormalizedGCDMonoid α] {s : Finset β} {f : βα} {b : β} (hb : b s) :
      s.gcd f f b
      theorem Finset.dvd_gcd {α : Type u_2} {β : Type u_3} [CancelCommMonoidWithZero α] [NormalizedGCDMonoid α] {s : Finset β} {f : βα} {a : α} :
      (∀ bs, a f b)a s.gcd f
      @[simp]
      theorem Finset.gcd_insert {α : Type u_2} {β : Type u_3} [CancelCommMonoidWithZero α] [NormalizedGCDMonoid α] {s : Finset β} {f : βα} [DecidableEq β] {b : β} :
      (insert b s).gcd f = gcd (f b) (s.gcd f)
      @[simp]
      theorem Finset.gcd_singleton {α : Type u_2} {β : Type u_3} [CancelCommMonoidWithZero α] [NormalizedGCDMonoid α] {f : βα} {b : β} :
      {b}.gcd f = normalize (f b)
      @[simp]
      theorem Finset.normalize_gcd {α : Type u_2} {β : Type u_3} [CancelCommMonoidWithZero α] [NormalizedGCDMonoid α] {s : Finset β} {f : βα} :
      normalize (s.gcd f) = s.gcd f
      theorem Finset.gcd_union {α : Type u_2} {β : Type u_3} [CancelCommMonoidWithZero α] [NormalizedGCDMonoid α] {s₁ : Finset β} {s₂ : Finset β} {f : βα} [DecidableEq β] :
      (s₁ s₂).gcd f = gcd (s₁.gcd f) (s₂.gcd f)
      theorem Finset.gcd_congr {α : Type u_2} {β : Type u_3} [CancelCommMonoidWithZero α] [NormalizedGCDMonoid α] {s₁ : Finset β} {s₂ : Finset β} {f : βα} {g : βα} (hs : s₁ = s₂) (hfg : as₂, f a = g a) :
      s₁.gcd f = s₂.gcd g
      theorem Finset.gcd_mono_fun {α : Type u_2} {β : Type u_3} [CancelCommMonoidWithZero α] [NormalizedGCDMonoid α] {s : Finset β} {f : βα} {g : βα} (h : bs, f b g b) :
      s.gcd f s.gcd g
      theorem Finset.gcd_mono {α : Type u_2} {β : Type u_3} [CancelCommMonoidWithZero α] [NormalizedGCDMonoid α] {s₁ : Finset β} {s₂ : Finset β} {f : βα} (h : s₁ s₂) :
      s₂.gcd f s₁.gcd f
      theorem Finset.gcd_image {α : Type u_2} {β : Type u_3} {γ : Type u_4} [CancelCommMonoidWithZero α] [NormalizedGCDMonoid α] {f : βα} [DecidableEq β] {g : γβ} (s : Finset γ) :
      (Finset.image g s).gcd f = s.gcd (f g)
      theorem Finset.gcd_eq_gcd_image {α : Type u_2} {β : Type u_3} [CancelCommMonoidWithZero α] [NormalizedGCDMonoid α] {s : Finset β} {f : βα} [DecidableEq α] :
      s.gcd f = (Finset.image f s).gcd id
      theorem Finset.gcd_eq_zero_iff {α : Type u_2} {β : Type u_3} [CancelCommMonoidWithZero α] [NormalizedGCDMonoid α] {s : Finset β} {f : βα} :
      s.gcd f = 0 xs, f x = 0
      theorem Finset.gcd_eq_gcd_filter_ne_zero {α : Type u_2} {β : Type u_3} [CancelCommMonoidWithZero α] [NormalizedGCDMonoid α] {s : Finset β} {f : βα} [DecidablePred fun (x : β) => f x = 0] :
      s.gcd f = (Finset.filter (fun (x : β) => f x 0) s).gcd f
      theorem Finset.gcd_mul_left {α : Type u_2} {β : Type u_3} [CancelCommMonoidWithZero α] [NormalizedGCDMonoid α] {s : Finset β} {f : βα} {a : α} :
      (s.gcd fun (x : β) => a * f x) = normalize a * s.gcd f
      theorem Finset.gcd_mul_right {α : Type u_2} {β : Type u_3} [CancelCommMonoidWithZero α] [NormalizedGCDMonoid α] {s : Finset β} {f : βα} {a : α} :
      (s.gcd fun (x : β) => f x * a) = s.gcd f * normalize a
      theorem Finset.extract_gcd' {α : Type u_2} {β : Type u_3} [CancelCommMonoidWithZero α] [NormalizedGCDMonoid α] {s : Finset β} (f : βα) (g : βα) (hs : xs, f x 0) (hg : bs, f b = s.gcd f * g b) :
      s.gcd g = 1
      theorem Finset.extract_gcd {α : Type u_2} {β : Type u_3} [CancelCommMonoidWithZero α] [NormalizedGCDMonoid α] {s : Finset β} (f : βα) (hs : s.Nonempty) :
      ∃ (g : βα), (∀ bs, f b = s.gcd f * g b) s.gcd g = 1
      theorem Finset.gcd_div_eq_one {ι : Type u_1} {α : Type u_2} [CancelCommMonoidWithZero α] [NormalizedGCDMonoid α] [Div α] [MulDivCancelClass α] {f : ια} {s : Finset ι} {i : ι} (his : i s) (hfi : f i 0) :
      (s.gcd fun (j : ι) => f j / s.gcd f) = 1

      Given a nonempty Finset s and a function f from s to , if d = s.gcd, then the gcd of (f i) / d is equal to 1.

      theorem Finset.gcd_div_id_eq_one {α : Type u_2} [CancelCommMonoidWithZero α] [NormalizedGCDMonoid α] [Div α] [MulDivCancelClass α] {s : Finset α} {a : α} (has : a s) (ha : a 0) :
      (s.gcd fun (b : α) => b / s.gcd id) = 1
      theorem Finset.gcd_eq_of_dvd_sub {α : Type u_2} {β : Type u_3} [CommRing α] [IsDomain α] [NormalizedGCDMonoid α] {s : Finset β} {f : βα} {g : βα} {a : α} (h : xs, a f x - g x) :
      gcd a (s.gcd f) = gcd a (s.gcd g)