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 #

source
def Multiset.lcm {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizedGCDMonoid α] (s : Multiset α) :
α

Least common multiple of a multiset

Equations
Instances For
    source
    @[simp]
    theorem Multiset.lcm_zero {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizedGCDMonoid α] :
    Multiset.lcm 0 = 1
    source
    @[simp]
    theorem Multiset.lcm_cons {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizedGCDMonoid α] (a : α) (s : Multiset α) :
    (a ::ₘ s).lcm = lcm a s.lcm
    source
    @[simp]
    theorem Multiset.lcm_singleton {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizedGCDMonoid α] {a : α} :
    {a}.lcm = normalize a
    source
    @[simp]
    theorem Multiset.lcm_add {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizedGCDMonoid α] (s₁ s₂ : Multiset α) :
    (s₁ + s₂).lcm = lcm s₁.lcm s₂.lcm
    source
    theorem Multiset.lcm_dvd {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizedGCDMonoid α] {s : Multiset α} {a : α} :
    s.lcm ∣ a ↔ ∀ b ∈ s, b ∣ a
    source
    theorem Multiset.dvd_lcm {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizedGCDMonoid α] {s : Multiset α} {a : α} (h : a ∈ s) :
    a ∣ s.lcm
    source
    theorem Multiset.lcm_mono {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizedGCDMonoid α] {s₁ s₂ : Multiset α} (h : s₁ ⊆ s₂) :
    s₁.lcm ∣ s₂.lcm
    source
    @[simp]
    theorem Multiset.normalize_lcm {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizedGCDMonoid α] (s : Multiset α) :
    normalize s.lcm = s.lcm
    source
    @[simp]
    theorem Multiset.lcm_eq_zero_iff {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizedGCDMonoid α] [Nontrivial α] (s : Multiset α) :
    s.lcm = 0 ↔ 0 ∈ s
    source
    @[simp]
    theorem Multiset.lcm_dedup {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizedGCDMonoid α] [DecidableEq α] (s : Multiset α) :
    s.dedup.lcm = s.lcm
    source
    @[simp]
    theorem Multiset.lcm_ndunion {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizedGCDMonoid α] [DecidableEq α] (s₁ s₂ : Multiset α) :
    (s₁.ndunion s₂).lcm = lcm s₁.lcm s₂.lcm
    source
    @[simp]
    theorem Multiset.lcm_union {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizedGCDMonoid α] [DecidableEq α] (s₁ s₂ : Multiset α) :
    (s₁ ∪ s₂).lcm = lcm s₁.lcm s₂.lcm
    source
    @[simp]
    theorem Multiset.lcm_ndinsert {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizedGCDMonoid α] [DecidableEq α] (a : α) (s : Multiset α) :
    (Multiset.ndinsert a s).lcm = lcm a s.lcm

    GCD #

    source
    def Multiset.gcd {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizedGCDMonoid α] (s : Multiset α) :
    α

    Greatest common divisor of a multiset

    Equations
    Instances For
      source
      @[simp]
      theorem Multiset.gcd_zero {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizedGCDMonoid α] :
      Multiset.gcd 0 = 0
      source
      @[simp]
      theorem Multiset.gcd_cons {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizedGCDMonoid α] (a : α) (s : Multiset α) :
      (a ::ₘ s).gcd = gcd a s.gcd
      source
      @[simp]
      theorem Multiset.gcd_singleton {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizedGCDMonoid α] {a : α} :
      {a}.gcd = normalize a
      source
      @[simp]
      theorem Multiset.gcd_add {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizedGCDMonoid α] (s₁ s₂ : Multiset α) :
      (s₁ + s₂).gcd = gcd s₁.gcd s₂.gcd
      source
      theorem Multiset.dvd_gcd {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizedGCDMonoid α] {s : Multiset α} {a : α} :
      a ∣ s.gcd ↔ ∀ b ∈ s, a ∣ b
      source
      theorem Multiset.gcd_dvd {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizedGCDMonoid α] {s : Multiset α} {a : α} (h : a ∈ s) :
      s.gcd ∣ a
      source
      theorem Multiset.gcd_mono {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizedGCDMonoid α] {s₁ s₂ : Multiset α} (h : s₁ ⊆ s₂) :
      s₂.gcd ∣ s₁.gcd
      source
      @[simp]
      theorem Multiset.normalize_gcd {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizedGCDMonoid α] (s : Multiset α) :
      normalize s.gcd = s.gcd
      source
      theorem Multiset.gcd_eq_zero_iff {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizedGCDMonoid α] (s : Multiset α) :
      s.gcd = 0 ↔ ∀ x ∈ s, x = 0
      source
      theorem Multiset.gcd_map_mul {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizedGCDMonoid α] (a : α) (s : Multiset α) :
      (Multiset.map (fun (x : α) => a * x) s).gcd = normalize a * s.gcd
      source
      @[simp]
      theorem Multiset.gcd_dedup {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizedGCDMonoid α] [DecidableEq α] (s : Multiset α) :
      s.dedup.gcd = s.gcd
      source
      @[simp]
      theorem Multiset.gcd_ndunion {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizedGCDMonoid α] [DecidableEq α] (s₁ s₂ : Multiset α) :
      (s₁.ndunion s₂).gcd = gcd s₁.gcd s₂.gcd
      source
      @[simp]
      theorem Multiset.gcd_union {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizedGCDMonoid α] [DecidableEq α] (s₁ s₂ : Multiset α) :
      (s₁ ∪ s₂).gcd = gcd s₁.gcd s₂.gcd
      source
      @[simp]
      theorem Multiset.gcd_ndinsert {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizedGCDMonoid α] [DecidableEq α] (a : α) (s : Multiset α) :
      (Multiset.ndinsert a s).gcd = gcd a s.gcd
      source
      theorem Multiset.extract_gcd' {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizedGCDMonoid α] (s t : Multiset α) (hs : ∃ x ∈ s, x ≠ 0) (ht : s = Multiset.map (fun (x : α) => s.gcd * x) t) :
      t.gcd = 1
      source
      theorem Multiset.extract_gcd {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizedGCDMonoid α] (s : Multiset α) (hs : s ≠ 0) :
      ∃ (t : Multiset α), s = Multiset.map (fun (x : α) => s.gcd * x) t ∧ t.gcd = 1