gcd_ndunion — Mathlib

English

The gcd of the ndunion is the gcd of the gcds: gcd(ndunion(s1,s2)) = gcd(s1.gcd, s2.gcd).

Русский

НОД ndunion равно gcd двух gcd: gcd(ndunion(s1,s2)) = gcd(s1.gcd, s2.gcd).

LaTeX

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

Lean4

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

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