gcd_union — Mathlib

English

The gcd of the union equals the gcd of the gcds: gcd(s1 ∪ s2) = gcd(s1.gcd, s2.gcd).

Русский

НОД объединения равен gcd gcd-значения: gcd(s1 ∪ s2) = gcd(s1.gcd, s2.gcd).

LaTeX

$$$(s_1 \cup s_2).\mathrm{gcd} = \mathrm{GCDMonoid.gcd}(s_1.\mathrm{gcd}, s_2.\mathrm{gcd})$$$

Lean4

@[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

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