lcm_union — Mathlib

English

For multisets s1 and s2, the least common multiple of their union equals the least common multiple of their individual least common multiples: lcm(s1 ∪ s2) = lcm(s1.lcm, s2.lcm).

Русский

Пусть мултисеты s1 и s2. Их объединение по операции ∪ имеет наименьшее общее кратное, равное наименьшему общему кратному их отдельных наибольших общих кратных: lcm(s1 ∪ s2) = lcm(s1.lcm, s2.lcm).

LaTeX

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

Lean4

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

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