lcm_union — Mathlib

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]

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