English
The lcm over the union of two finite sets s1 and s2 is the lcm of the lcms over each set.
Русский
НОК объединения двух конечных множеств равен НОК по НОКам одних и других множеств.
LaTeX
$$$((s_1 \cup s_2).lcm f) = \operatorname{lcm}(s_1.lcm f, s_2.lcm f)$$$
Lean4
theorem lcm_union [DecidableEq β] : (s₁ ∪ s₂).lcm f = GCDMonoid.lcm (s₁.lcm f) (s₂.lcm f) :=
Finset.induction_on s₁ (by rw [empty_union, lcm_empty, lcm_one_left, normalize_lcm]) fun a s _ ih ↦ by
rw [insert_union, lcm_insert, lcm_insert, ih, lcm_assoc]