English
The lcm of two positive integers corresponds to the supremum of their prime factor multisets, i.e., factorMultiset(lcm(m,n)) = factorMultiset(m) ⊔ factorMultiset(n).
Русский
НОК двух положительных чисел соответствует сумипремуму их мультсет-факторизаций: factorMultiset(lcm(m,n)) = factorMultiset(m) ⊔ factorMultiset(n).
LaTeX
$$$ \\operatorname{factorMultiset}(\\operatorname{lcm}(m,n)) = \\operatorname{factorMultiset}(m) \\sqcup \\operatorname{factorMultiset}(n) $$$
Lean4
theorem factorMultiset_lcm (m n : ℕ+) : factorMultiset (lcm m n) = factorMultiset m ⊔ factorMultiset n :=
by
apply le_antisymm
· rw [← PrimeMultiset.prod_dvd_iff, prod_factorMultiset]
apply lcm_dvd <;> rw [← factorMultiset_le_iff']
· exact le_sup_left
· exact le_sup_right
· apply sup_le_iff.mpr; constructor <;> apply factorMultiset_le_iff.mpr
· exact dvd_lcm_left m n
· exact dvd_lcm_right m n
