English
For any two prime multisets u and v, the product of their inf is the gcd of the products: (u ⊓ v).prod = gcd(u.prod, v.prod).
Русский
Для любых мультсетов простых u и v произведение их инфимума равно НОД их произведений: (u ⊓ v).prod = gcd(u.prod, v.prod).
LaTeX
$$$ (u \\inf v).prod = \\gcd(u.prod, v.prod) $$$
Lean4
theorem prod_inf (u v : PrimeMultiset) : (u ⊓ v).prod = PNat.gcd u.prod v.prod :=
by
let n := u.prod
let m := v.prod
change (u ⊓ v).prod = PNat.gcd 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_gcd n m, PNat.prod_factorMultiset]
