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

Least common multiple of a finite set

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

    gcd #

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

    Greatest common divisor of a finite set

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