English
For prime multisets u and v, the product of their supremum equals the lcm of their products: (u ⊔ v).prod = lcm(u.prod, v.prod).
Русский
Для мультсетов простых u и v произведение их суперимумa равно НОК их произведений: (u ⊔ v).prod = lcm(u.prod, v.prod).
LaTeX
$$$ (u \\sup v).prod = \\operatorname{lcm}(u.prod, v.prod) $$$
Lean4
theorem prod_sup (u v : PrimeMultiset) : (u ⊔ v).prod = PNat.lcm u.prod v.prod :=
by
let n := u.prod
let m := v.prod
change (u ⊔ v).prod = PNat.lcm n m
have : u = n.factorMultiset := u.factorMultiset_prod.symm; rw [this]
have : v = m.factorMultiset := v.factorMultiset_prod.symm; rw [this]
rw [← PNat.factorMultiset_lcm n m, PNat.prod_factorMultiset]
