Mathlib.Algebra.GCDMonoid.Multiset

Multiset.lcm definition

(s : Multiset α) : α

Full source

/-- Least common multiple of a multiset -/
def lcm (s : Multiset α) : α :=
  s.fold GCDMonoid.lcm 1

Least common multiple of a multiset

Informal description

The least common multiple of a multiset $ s $ of elements in a normalized GCD monoid $ \alpha $ is defined by folding the `lcm` operation over the multiset starting with the multiplicative identity $ 1 $. More precisely, for a multiset $ s = \{a_1, \ldots, a_n\} $, the least common multiple is computed as: \[ \mathrm{lcm}(a_1, \mathrm{lcm}(a_2, \ldots, \mathrm{lcm}(a_n, 1) \ldots)). \]

Multiset.lcm_zero theorem

: (0 : Multiset α).lcm = 1

Full source

@[simp]
theorem lcm_zero : (0 : Multiset α).lcm = 1 :=
  fold_zero _ _

Least Common Multiple of Empty Multiset is One

Informal description

The least common multiple of the empty multiset in a normalized GCD monoid $\alpha$ is equal to the multiplicative identity $1$, i.e., $\mathrm{lcm}(\emptyset) = 1$.

Multiset.lcm_cons theorem

(a : α) (s : Multiset α) : (a ::ₘ s).lcm = GCDMonoid.lcm a s.lcm

Full source

@[simp]
theorem lcm_cons (a : α) (s : Multiset α) : (a ::ₘ s).lcm = GCDMonoid.lcm a s.lcm :=
  fold_cons_left _ _ _ _

Least Common Multiple of Multiset with Added Element: $\mathrm{lcm}(a \cdot s) = \mathrm{lcm}(a, \mathrm{lcm}(s))$

Informal description

For any element $a$ in a normalized GCD monoid $\alpha$ and any multiset $s$ of elements of $\alpha$, the least common multiple of the multiset obtained by adding $a$ to $s$ is equal to the least common multiple of $a$ and the least common multiple of $s$. That is: \[ \mathrm{lcm}(a \cdot s) = \mathrm{lcm}(a, \mathrm{lcm}(s)). \]

Multiset.lcm_singleton theorem

{a : α} : ({ a } : Multiset α).lcm = normalize a

Full source

@[simp]
theorem lcm_singleton {a : α} : ({a} : Multiset α).lcm = normalize a :=
  (fold_singleton _ _ _).trans <| lcm_one_right _

Least Common Multiple of Singleton Multiset Equals Normalization

Informal description

For any element $a$ in a normalized GCD monoid $\alpha$, the least common multiple of the singleton multiset $\{a\}$ is equal to the normalized form of $a$, i.e., $\mathrm{lcm}(\{a\}) = \mathrm{normalize}(a)$.

Multiset.lcm_add theorem

(s₁ s₂ : Multiset α) : (s₁ + s₂).lcm = GCDMonoid.lcm s₁.lcm s₂.lcm

Full source

@[simp]
theorem lcm_add (s₁ s₂ : Multiset α) : (s₁ + s₂).lcm = GCDMonoid.lcm s₁.lcm s₂.lcm :=
  Eq.trans (by simp [lcm]) (fold_add _ _ _ _ _)

Least Common Multiple of Multiset Union: $\mathrm{lcm}(s_1 + s_2) = \mathrm{lcm}(\mathrm{lcm}(s_1), \mathrm{lcm}(s_2))$

Informal description

For any two multisets $s_1$ and $s_2$ of elements in a normalized GCD monoid $\alpha$, the least common multiple of their sum $s_1 + s_2$ is equal to the least common multiple of the least common multiples of $s_1$ and $s_2$ individually. That is, \[ \mathrm{lcm}(s_1 + s_2) = \mathrm{lcm}(\mathrm{lcm}(s_1), \mathrm{lcm}(s_2)). \]

Multiset.lcm_dvd theorem

{s : Multiset α} {a : α} : s.lcm ∣ a ↔ ∀ b ∈ s, b ∣ a

Full source

theorem lcm_dvd {s : Multiset α} {a : α} : s.lcm ∣ as.lcm ∣ a ↔ ∀ b ∈ s, b ∣ a :=
  Multiset.induction_on s (by simp)
    (by simp +contextual [or_imp, forall_and, lcm_dvd_iff])

Least Common Multiple Divisibility Criterion for Multisets: $\mathrm{lcm}(s) \mid a \leftrightarrow \forall b \in s, b \mid a$

Informal description

For any multiset $s$ of elements in a normalized GCD monoid $\alpha$ and any element $a \in \alpha$, the least common multiple of $s$ divides $a$ if and only if every element $b \in s$ divides $a$. That is, \[ \mathrm{lcm}(s) \mid a \leftrightarrow \forall b \in s, b \mid a. \]

Multiset.dvd_lcm theorem

{s : Multiset α} {a : α} (h : a ∈ s) : a ∣ s.lcm

Full source

theorem dvd_lcm {s : Multiset α} {a : α} (h : a ∈ s) : a ∣ s.lcm :=
  lcm_dvd.1 dvd_rfl _ h

Element Divides Multiset LCM: $a \mid \mathrm{lcm}(s)$ for $a \in s$

Informal description

For any multiset $s$ of elements in a normalized GCD monoid $\alpha$ and any element $a \in s$, the element $a$ divides the least common multiple of $s$, i.e., $a \mid \mathrm{lcm}(s)$.

Multiset.lcm_mono theorem

{s₁ s₂ : Multiset α} (h : s₁ ⊆ s₂) : s₁.lcm ∣ s₂.lcm

Full source

theorem lcm_mono {s₁ s₂ : Multiset α} (h : s₁ ⊆ s₂) : s₁.lcm ∣ s₂.lcm :=
  lcm_dvd.2 fun _ hb ↦ dvd_lcm (h hb)

Monotonicity of LCM with respect to multiset inclusion: $\mathrm{lcm}(s_1) \mid \mathrm{lcm}(s_2)$ for $s_1 \subseteq s_2$

Informal description

For any two multisets $s_1$ and $s_2$ over a normalized GCD monoid $\alpha$, if $s_1$ is a subset of $s_2$ (i.e., every element of $s_1$ appears in $s_2$ with at least the same multiplicity), then the least common multiple of $s_1$ divides the least common multiple of $s_2$, i.e., $\mathrm{lcm}(s_1) \mid \mathrm{lcm}(s_2)$.

Multiset.normalize_lcm theorem

(s : Multiset α) : normalize s.lcm = s.lcm

Full source

@[simp]
theorem normalize_lcm (s : Multiset α) : normalize s.lcm = s.lcm :=
  Multiset.induction_on s (by simp) fun a s _ ↦ by simp

Normalization of Multiset Least Common Multiple: $\text{normalize}(\text{lcm}(s)) = \text{lcm}(s)$

Informal description

For any multiset $s$ of elements in a normalized GCD monoid $\alpha$, the normalization of the least common multiple of $s$ is equal to the least common multiple itself, i.e., $\text{normalize}(\text{lcm}(s)) = \text{lcm}(s)$.

Multiset.lcm_eq_zero_iff theorem

[Nontrivial α] (s : Multiset α) : s.lcm = 0 ↔ (0 : α) ∈ s

Full source

@[simp]
nonrec theorem lcm_eq_zero_iff [Nontrivial α] (s : Multiset α) : s.lcm = 0 ↔ (0 : α) ∈ s := by
  induction s using Multiset.induction_on with
  | empty => simp only [lcm_zero, one_ne_zero, not_mem_zero]
  | cons a s ihs => simp only [mem_cons, lcm_cons, lcm_eq_zero_iff, ihs, @eq_comm _ a]

$\mathrm{lcm}(s) = 0$ iff $0 \in s$ in a nontrivial GCD monoid

Informal description

For a nontrivial normalized GCD monoid $\alpha$ and a multiset $s$ of elements of $\alpha$, the least common multiple of $s$ is zero if and only if $0$ is an element of $s$. In other words: \[ \mathrm{lcm}(s) = 0 \leftrightarrow 0 \in s. \]

Multiset.lcm_dedup theorem

(s : Multiset α) : (dedup s).lcm = s.lcm

Full source

@[simp]
theorem lcm_dedup (s : Multiset α) : (dedup s).lcm = s.lcm :=
  Multiset.induction_on s (by simp) fun a s IH ↦ by
    by_cases h : a ∈ s <;> simp [IH, h]
    unfold lcm
    rw [← cons_erase h, fold_cons_left, ← lcm_assoc, lcm_same]
    apply lcm_eq_of_associated_left (associated_normalize _)

Least Common Multiple Invariance Under Deduplication: $\mathrm{lcm}(\mathrm{dedup}(s)) = \mathrm{lcm}(s)$

Informal description

For any multiset $s$ of elements in a normalized GCD monoid $\alpha$, the least common multiple of the deduplicated multiset $\mathrm{dedup}(s)$ is equal to the least common multiple of $s$ itself, i.e., \[ \mathrm{lcm}(\mathrm{dedup}(s)) = \mathrm{lcm}(s). \]

Multiset.lcm_ndunion theorem

(s₁ s₂ : Multiset α) : (ndunion s₁ s₂).lcm = GCDMonoid.lcm s₁.lcm s₂.lcm

Full source

@[simp]
theorem lcm_ndunion (s₁ s₂ : Multiset α) : (ndunion s₁ s₂).lcm = GCDMonoid.lcm s₁.lcm s₂.lcm := by
  rw [← lcm_dedup, dedup_ext.2, lcm_dedup, lcm_add]
  simp

Least Common Multiple of Non-Duplicating Multiset Union: $\mathrm{lcm}(\mathrm{ndunion}(s_1, s_2)) = \mathrm{lcm}(\mathrm{lcm}(s_1), \mathrm{lcm}(s_2))$

Informal description

For any two multisets $s_1$ and $s_2$ of elements in a normalized GCD monoid $\alpha$, the least common multiple of their non-duplicating union $\mathrm{ndunion}(s_1, s_2)$ is equal to the least common multiple of the least common multiples of $s_1$ and $s_2$ individually. That is, \[ \mathrm{lcm}(\mathrm{ndunion}(s_1, s_2)) = \mathrm{lcm}(\mathrm{lcm}(s_1), \mathrm{lcm}(s_2)). \]

Multiset.lcm_union theorem

(s₁ s₂ : Multiset α) : (s₁ ∪ s₂).lcm = GCDMonoid.lcm s₁.lcm s₂.lcm

Full source

@[simp]
theorem lcm_union (s₁ s₂ : Multiset α) : (s₁ ∪ s₂).lcm = GCDMonoid.lcm s₁.lcm s₂.lcm := by
  rw [← lcm_dedup, dedup_ext.2, lcm_dedup, lcm_add]
  simp

Least Common Multiple of Multiset Union: $\mathrm{lcm}(s_1 \cup s_2) = \mathrm{lcm}(\mathrm{lcm}(s_1), \mathrm{lcm}(s_2))$

Informal description

For any two multisets $s_1$ and $s_2$ of elements in a normalized GCD monoid $\alpha$, the least common multiple of their union $s_1 \cup s_2$ is equal to the least common multiple of the least common multiples of $s_1$ and $s_2$ individually. That is, \[ \mathrm{lcm}(s_1 \cup s_2) = \mathrm{lcm}(\mathrm{lcm}(s_1), \mathrm{lcm}(s_2)). \]

Multiset.lcm_ndinsert theorem

(a : α) (s : Multiset α) : (ndinsert a s).lcm = GCDMonoid.lcm a s.lcm

Full source

@[simp]
theorem lcm_ndinsert (a : α) (s : Multiset α) : (ndinsert a s).lcm = GCDMonoid.lcm a s.lcm := by
  rw [← lcm_dedup, dedup_ext.2, lcm_dedup, lcm_cons]
  simp

Least Common Multiple of Multiset Insertion: $\mathrm{lcm}(\mathrm{ndinsert}(a, s)) = \mathrm{lcm}(a, \mathrm{lcm}(s))$

Informal description

For any element $a$ in a normalized GCD monoid $\alpha$ and any multiset $s$ of elements of $\alpha$, the least common multiple of the multiset obtained by inserting $a$ into $s$ (ignoring multiplicities) is equal to the least common multiple of $a$ and the least common multiple of $s$. That is: \[ \mathrm{lcm}(\mathrm{ndinsert}(a, s)) = \mathrm{lcm}(a, \mathrm{lcm}(s)). \]

Multiset.gcd definition

(s : Multiset α) : α

Full source

/-- Greatest common divisor of a multiset -/
def gcd (s : Multiset α) : α :=
  s.fold GCDMonoid.gcd 0

Greatest common divisor of a multiset

Informal description

The greatest common divisor (gcd) of a multiset $ s $ of elements from a normalized GCD monoid $ \alpha $ is defined by folding the binary gcd operation over the multiset, starting with the element $ 0 $.

Multiset.gcd_zero theorem

: (0 : Multiset α).gcd = 0

Full source

@[simp]
theorem gcd_zero : (0 : Multiset α).gcd = 0 :=
  fold_zero _ _

GCD of Empty Multiset is Zero

Informal description

The greatest common divisor of the empty multiset in a normalized GCD monoid $\alpha$ is $0$, i.e., $\gcd(\emptyset) = 0$.

Multiset.gcd_cons theorem

(a : α) (s : Multiset α) : (a ::ₘ s).gcd = GCDMonoid.gcd a s.gcd

Full source

@[simp]
theorem gcd_cons (a : α) (s : Multiset α) : (a ::ₘ s).gcd = GCDMonoid.gcd a s.gcd :=
  fold_cons_left _ _ _ _

GCD of a Multiset After Insertion: $\gcd(a \cdot s) = \gcd(a, \gcd(s))$

Informal description

For any element $a$ in a normalized GCD monoid $\alpha$ and any multiset $s$ of elements of $\alpha$, the greatest common divisor of the multiset obtained by adding $a$ to $s$ equals the greatest common divisor of $a$ and the greatest common divisor of $s$. That is, $\gcd(a \cdot s) = \gcd(a, \gcd(s))$.

Multiset.gcd_singleton theorem

{a : α} : ({ a } : Multiset α).gcd = normalize a

Full source

@[simp]
theorem gcd_singleton {a : α} : ({a} : Multiset α).gcd = normalize a :=
  (fold_singleton _ _ _).trans <| gcd_zero_right _

GCD of Singleton Multiset Equals Normalization

Informal description

For any element $a$ in a normalized GCD monoid $\alpha$, the greatest common divisor of the singleton multiset $\{a\}$ equals the normalization of $a$, i.e., $\gcd(\{a\}) = \mathrm{normalize}(a)$.

Multiset.gcd_add theorem

(s₁ s₂ : Multiset α) : (s₁ + s₂).gcd = GCDMonoid.gcd s₁.gcd s₂.gcd

Full source

@[simp]
theorem gcd_add (s₁ s₂ : Multiset α) : (s₁ + s₂).gcd = GCDMonoid.gcd s₁.gcd s₂.gcd :=
  Eq.trans (by simp [gcd]) (fold_add _ _ _ _ _)

GCD of Multiset Union: $\text{gcd}(s₁ + s₂) = \text{gcd}(\text{gcd}(s₁), \text{gcd}(s₂))$

Informal description

For any two multisets $s₁$ and $s₂$ over a normalized GCD monoid $\alpha$, the greatest common divisor of their union $s₁ + s₂$ equals the greatest common divisor of the greatest common divisors of $s₁$ and $s₂$, i.e., \[ \text{gcd}(s₁ + s₂) = \text{gcd}(\text{gcd}(s₁), \text{gcd}(s₂)). \]

Multiset.dvd_gcd theorem

{s : Multiset α} {a : α} : a ∣ s.gcd ↔ ∀ b ∈ s, a ∣ b

Full source

theorem dvd_gcd {s : Multiset α} {a : α} : a ∣ s.gcda ∣ s.gcd ↔ ∀ b ∈ s, a ∣ b :=
  Multiset.induction_on s (by simp)
    (by simp +contextual [or_imp, forall_and, dvd_gcd_iff])

Divisibility Condition for GCD of a Multiset: $a \mid \gcd(s) \leftrightarrow \forall b \in s, a \mid b$

Informal description

For any multiset $s$ over a normalized GCD monoid $\alpha$ and any element $a \in \alpha$, $a$ divides the greatest common divisor of $s$ if and only if $a$ divides every element of $s$. In symbols: \[ a \mid \gcd(s) \leftrightarrow \forall b \in s, a \mid b. \]

Multiset.gcd_dvd theorem

{s : Multiset α} {a : α} (h : a ∈ s) : s.gcd ∣ a

Full source

theorem gcd_dvd {s : Multiset α} {a : α} (h : a ∈ s) : s.gcd ∣ a :=
  dvd_gcd.1 dvd_rfl _ h

GCD of Multiset Divides Its Elements: $\gcd(s) \mid a$ for $a \in s$

Informal description

For any multiset $s$ over a normalized GCD monoid $\alpha$ and any element $a \in s$, the greatest common divisor of $s$ divides $a$, i.e., $\gcd(s) \mid a$.

Multiset.gcd_mono theorem

{s₁ s₂ : Multiset α} (h : s₁ ⊆ s₂) : s₂.gcd ∣ s₁.gcd

Full source

theorem gcd_mono {s₁ s₂ : Multiset α} (h : s₁ ⊆ s₂) : s₂.gcd ∣ s₁.gcd :=
  dvd_gcd.2 fun _ hb ↦ gcd_dvd (h hb)

Monotonicity of GCD under Multiset Inclusion: $\gcd(s₂) \mid \gcd(s₁)$ when $s₁ \subseteq s₂$

Informal description

For any two multisets $s₁$ and $s₂$ over a normalized GCD monoid $\alpha$, if $s₁$ is a subset of $s₂$, then the greatest common divisor of $s₂$ divides the greatest common divisor of $s₁$, i.e., $\gcd(s₂) \mid \gcd(s₁)$.

Multiset.normalize_gcd theorem

(s : Multiset α) : normalize s.gcd = s.gcd

Full source

@[simp]
theorem normalize_gcd (s : Multiset α) : normalize s.gcd = s.gcd :=
  Multiset.induction_on s (by simp) fun a s _ ↦ by simp

Normalization of Multiset GCD: $\mathrm{normalize}(\gcd(s)) = \gcd(s)$

Informal description

For any multiset $s$ of elements in a normalized GCD monoid $\alpha$, the normalized form of the greatest common divisor of $s$ is equal to the greatest common divisor itself, i.e., $\mathrm{normalize}(\gcd(s)) = \gcd(s)$.

Multiset.gcd_eq_zero_iff theorem

(s : Multiset α) : s.gcd = 0 ↔ ∀ x : α, x ∈ s → x = 0

Full source

theorem gcd_eq_zero_iff (s : Multiset α) : s.gcd = 0 ↔ ∀ x : α, x ∈ s → x = 0 := by
  constructor
  · intro h x hx
    apply eq_zero_of_zero_dvd
    rw [← h]
    apply gcd_dvd hx
  · refine s.induction_on ?_ ?_
    · simp
    intro a s sgcd h
    simp [h a (mem_cons_self a s), sgcd fun x hx ↦ h x (mem_cons_of_mem hx)]

GCD of Multiset is Zero if and only if All Elements are Zero

Informal description

For any multiset $s$ of elements in a normalized GCD monoid $\alpha$, the greatest common divisor of $s$ is zero if and only if every element $x \in s$ is zero. That is, $$\gcd(s) = 0 \leftrightarrow \forall x \in s, x = 0.$$

Multiset.gcd_map_mul theorem

(a : α) (s : Multiset α) : (s.map (a * ·)).gcd = normalize a * s.gcd

Full source

theorem gcd_map_mul (a : α) (s : Multiset α) : (s.map (a * ·)).gcd = normalize a * s.gcd := by
  refine s.induction_on ?_ fun b s ih ↦ ?_
  · simp_rw [map_zero, gcd_zero, mul_zero]
  · simp_rw [map_cons, gcd_cons, ← gcd_mul_left]
    rw [ih]
    apply ((normalize_associated a).mul_right _).gcd_eq_right

GCD of Scaled Multiset: $\gcd(a \cdot s) = \text{normalize}(a) \cdot \gcd(s)$

Informal description

Let $\alpha$ be a normalized GCD monoid. For any element $a \in \alpha$ and any multiset $s$ of elements of $\alpha$, the greatest common divisor of the multiset obtained by multiplying each element of $s$ by $a$ equals the normalized form of $a$ multiplied by the greatest common divisor of $s$. That is, $$\gcd(\{a \cdot x \mid x \in s\}) = \text{normalize}(a) \cdot \gcd(s).$$

Multiset.gcd_dedup theorem

(s : Multiset α) : (dedup s).gcd = s.gcd

Full source

@[simp]
theorem gcd_dedup (s : Multiset α) : (dedup s).gcd = s.gcd :=
  Multiset.induction_on s (by simp) fun a s IH ↦ by
    by_cases h : a ∈ s <;> simp [IH, h]
    unfold gcd
    rw [← cons_erase h, fold_cons_left, ← gcd_assoc, gcd_same]
    apply (associated_normalize _).gcd_eq_left

GCD Invariance Under Deduplication: $\gcd(\text{dedup}(s)) = \gcd(s)$

Informal description

For any multiset $s$ of elements in a normalized GCD monoid $\alpha$, the greatest common divisor of the deduplicated multiset $\text{dedup}(s)$ is equal to the greatest common divisor of $s$ itself, i.e., $\gcd(\text{dedup}(s)) = \gcd(s)$.

Multiset.gcd_ndunion theorem

(s₁ s₂ : Multiset α) : (ndunion s₁ s₂).gcd = GCDMonoid.gcd s₁.gcd s₂.gcd

Full source

@[simp]
theorem gcd_ndunion (s₁ s₂ : Multiset α) : (ndunion s₁ s₂).gcd = GCDMonoid.gcd s₁.gcd s₂.gcd := by
  rw [← gcd_dedup, dedup_ext.2, gcd_dedup, gcd_add]
  simp

GCD of Nondisjoint Union: $\gcd(\text{ndunion}(s₁, s₂)) = \gcd(\gcd(s₁), \gcd(s₂))$

Informal description

For any two multisets $s₁$ and $s₂$ over a normalized GCD monoid $\alpha$, the greatest common divisor of their nondisjoint union $\text{ndunion}(s₁, s₂)$ equals the greatest common divisor of the greatest common divisors of $s₁$ and $s₂$, i.e., \[ \gcd(\text{ndunion}(s₁, s₂)) = \gcd(\gcd(s₁), \gcd(s₂)). \]

Multiset.gcd_union theorem

(s₁ s₂ : Multiset α) : (s₁ ∪ s₂).gcd = GCDMonoid.gcd s₁.gcd s₂.gcd

Full source

@[simp]
theorem gcd_union (s₁ s₂ : Multiset α) : (s₁ ∪ s₂).gcd = GCDMonoid.gcd s₁.gcd s₂.gcd := by
  rw [← gcd_dedup, dedup_ext.2, gcd_dedup, gcd_add]
  simp

GCD of Multiset Union: $\gcd(s₁ \cup s₂) = \gcd(\gcd(s₁), \gcd(s₂))$

Informal description

For any two multisets $s₁$ and $s₂$ over a normalized GCD monoid $\alpha$, the greatest common divisor of their union $s₁ \cup s₂$ equals the greatest common divisor of the greatest common divisors of $s₁$ and $s₂$, i.e., \[ \gcd(s₁ \cup s₂) = \gcd(\gcd(s₁), \gcd(s₂)). \]

Multiset.gcd_ndinsert theorem

(a : α) (s : Multiset α) : (ndinsert a s).gcd = GCDMonoid.gcd a s.gcd

Full source

@[simp]
theorem gcd_ndinsert (a : α) (s : Multiset α) : (ndinsert a s).gcd = GCDMonoid.gcd a s.gcd := by
  rw [← gcd_dedup, dedup_ext.2, gcd_dedup, gcd_cons]
  simp

GCD of Multiset After Insertion: $\gcd(\text{ndinsert}(a, s)) = \gcd(a, \gcd(s))$

Informal description

For any element $a$ in a normalized GCD monoid $\alpha$ and any multiset $s$ of elements of $\alpha$, the greatest common divisor of the multiset obtained by inserting $a$ into $s$ (ignoring multiplicities) equals the greatest common divisor of $a$ and the greatest common divisor of $s$. That is, $\gcd(\text{ndinsert}(a, s)) = \gcd(a, \gcd(s))$.

Multiset.extract_gcd' theorem

(s t : Multiset α) (hs : ∃ x, x ∈ s ∧ x ≠ (0 : α)) (ht : s = t.map (s.gcd * ·)) : t.gcd = 1

Full source

theorem extract_gcd' (s t : Multiset α) (hs : ∃ x, x ∈ s ∧ x ≠ (0 : α))
    (ht : s = t.map (s.gcd * ·)) : t.gcd = 1 :=
  ((@mul_right_eq_self₀ _ _ s.gcd _).1 <| by
        conv_lhs => rw [← normalize_gcd, ← gcd_map_mul, ← ht]).resolve_right <| by
    contrapose! hs
    exact s.gcd_eq_zero_iff.1 hs

GCD Factorization Property for Multisets: $\gcd(t) = 1$ when $s = \gcd(s) \cdot t$ and $s$ contains a nonzero element

Informal description

Let $\alpha$ be a normalized GCD monoid. For any multisets $s$ and $t$ of elements of $\alpha$, if there exists a nonzero element in $s$ (i.e., $\exists x \in s, x \neq 0$) and $s$ can be expressed as $t$ with each element multiplied by $\gcd(s)$ (i.e., $s = \{ \gcd(s) \cdot y \mid y \in t \}$), then the greatest common divisor of $t$ is $1$.

Multiset.extract_gcd theorem

(s : Multiset α) (hs : s ≠ 0) : ∃ t : Multiset α, s = t.map (s.gcd * ·) ∧ t.gcd = 1

Full source

theorem extract_gcd (s : Multiset α) (hs : s ≠ 0) :
    ∃ t : Multiset α, s = t.map (s.gcd * ·) ∧ t.gcd = 1 := by
  classical
    by_cases h : ∀ x ∈ s, x = (0 : α)
    · use replicate (card s) 1
      rw [map_replicate, eq_replicate, mul_one, s.gcd_eq_zero_iff.2 h, ← nsmul_singleton,
    ← gcd_dedup, dedup_nsmul (card_pos.2 hs).ne', dedup_singleton, gcd_singleton]
      exact ⟨⟨rfl, h⟩, normalize_one⟩
    · choose f hf using @gcd_dvd _ _ _ s
      push_neg at h
      refine ⟨s.pmap @f fun _ ↦ id, ?_, extract_gcd' s _ h ?_⟩ <;>
      · rw [map_pmap]
        conv_lhs => rw [← s.map_id, ← s.pmap_eq_map _ _ fun _ ↦ id]
        congr with (x hx)
        rw [id, ← hf hx]

Factorization of Multiset by GCD: $s = \gcd(s) \cdot t$ with $\gcd(t) = 1$ for $s \neq 0$

Informal description

For any nonempty multiset $s$ of elements in a normalized GCD monoid $\alpha$, there exists a multiset $t$ such that $s$ can be expressed as the image of $t$ under the function $\lambda x, \gcd(s) \cdot x$, and the greatest common divisor of $t$ is $1$. That is, there exists $t$ with: \[ s = \{ \gcd(s) \cdot y \mid y \in t \} \quad \text{and} \quad \gcd(t) = 1. \]

Mathlib.Algebra.GCDMonoid.Multiset

Main definitions

Implementation notes

Tags