Documentation

Mathlib.Algebra.GCDMonoid.Multiset

GCD and LCM operations on multisets #

Main definitions #

Implementation notes #

TODO: simplify with a tactic and Data.Multiset.Lattice

Tags #

multiset, gcd

LCM #

Least common multiple of a multiset

Equations
Instances For
    @[simp]
    @[simp]
    theorem Multiset.lcm_singleton {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizedGCDMonoid α] {a : α} :
    Multiset.lcm {a} = normalize a
    @[simp]
    theorem Multiset.lcm_add {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizedGCDMonoid α] (s₁ : Multiset α) (s₂ : Multiset α) :
    Multiset.lcm (s₁ + s₂) = lcm (Multiset.lcm s₁) (Multiset.lcm s₂)
    theorem Multiset.lcm_dvd {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizedGCDMonoid α] {s : Multiset α} {a : α} :
    Multiset.lcm s a ∀ (b : α), b sb a
    theorem Multiset.dvd_lcm {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizedGCDMonoid α] {s : Multiset α} {a : α} (h : a s) :
    theorem Multiset.lcm_mono {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizedGCDMonoid α] {s₁ : Multiset α} {s₂ : Multiset α} (h : s₁ s₂) :
    @[simp]
    @[simp]
    @[simp]
    theorem Multiset.lcm_union {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizedGCDMonoid α] [DecidableEq α] (s₁ : Multiset α) (s₂ : Multiset α) :
    Multiset.lcm (s₁ s₂) = lcm (Multiset.lcm s₁) (Multiset.lcm s₂)

    GCD #

    Greatest common divisor of a multiset

    Equations
    Instances For
      @[simp]
      @[simp]
      theorem Multiset.gcd_singleton {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizedGCDMonoid α] {a : α} :
      Multiset.gcd {a} = normalize a
      @[simp]
      theorem Multiset.gcd_add {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizedGCDMonoid α] (s₁ : Multiset α) (s₂ : Multiset α) :
      Multiset.gcd (s₁ + s₂) = gcd (Multiset.gcd s₁) (Multiset.gcd s₂)
      theorem Multiset.dvd_gcd {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizedGCDMonoid α] {s : Multiset α} {a : α} :
      a Multiset.gcd s ∀ (b : α), b sa b
      theorem Multiset.gcd_dvd {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizedGCDMonoid α] {s : Multiset α} {a : α} (h : a s) :
      theorem Multiset.gcd_mono {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizedGCDMonoid α] {s₁ : Multiset α} {s₂ : Multiset α} (h : s₁ s₂) :
      @[simp]
      theorem Multiset.gcd_eq_zero_iff {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizedGCDMonoid α] (s : Multiset α) :
      Multiset.gcd s = 0 ∀ (x : α), x sx = 0
      theorem Multiset.gcd_map_mul {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizedGCDMonoid α] (a : α) (s : Multiset α) :
      Multiset.gcd (Multiset.map ((fun x x_1 => x * x_1) a) s) = normalize a * Multiset.gcd s
      @[simp]
      @[simp]
      theorem Multiset.gcd_union {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizedGCDMonoid α] [DecidableEq α] (s₁ : Multiset α) (s₂ : Multiset α) :
      Multiset.gcd (s₁ s₂) = gcd (Multiset.gcd s₁) (Multiset.gcd s₂)
      theorem Multiset.extract_gcd' {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizedGCDMonoid α] (s : Multiset α) (t : Multiset α) (hs : x, x s x 0) (ht : s = Multiset.map ((fun x x_1 => x * x_1) (Multiset.gcd s)) t) :
      theorem Multiset.extract_gcd {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizedGCDMonoid α] (s : Multiset α) (hs : s 0) :
      t, s = Multiset.map ((fun x x_1 => x * x_1) (Multiset.gcd s)) t Multiset.gcd t = 1