gcd_dedup — Mathlib

English

Taking gcd commutes with dedup: gcd(dedup(s)) = gcd(s).

Русский

НОД коммутирует с удалением повторов: gcd(dedup(s)) = gcd(s).

LaTeX

$$$(\mathrm{dedup} s).\mathrm{gcd} = s.\mathrm{gcd}$$$

Lean4

@[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; swap; · simp [IH, h]
    simp only [h, dedup_cons_of_mem, IH, gcd_cons]
    unfold gcd
    rw [← cons_erase h, fold_cons_left, ← gcd_assoc, gcd_same]
    apply (associated_normalize _).gcd_eq_left

Похожие утверждения