English
Let α be as above and s1, s2 multisets. The least common multiple of their ndunion equals the least common multiple of their individual least common multiples: lcm(ndunion(s1, s2)) = lcm(s1.lcm, s2.lcm).
Русский
Пусть α удовлетворяет условиям. Тогда наименьшее общее кратное объединения ndunion двух мультисетов равно наименьшему общему кратному их отдельных наименьших общих кратных: lcm(ndunion(s1, s2)) = lcm(s1.lcm, s2.lcm).
LaTeX
$$$(\mathrm{ndunion}(s_1,s_2)).\mathrm{lcm} = \mathrm{GCDMonoid.lcm}(s_1.\mathrm{lcm}, s_2.\mathrm{lcm})$$$
Lean4
@[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
