English
The gcd of two positive integers corresponds to the infimum of their prime factor multisets, i.e., factorMultiset(gcd(m,n)) = factorMultiset(m) ⊓ factorMultiset(n).
Русский
НОД двух положительных чисел соответствует инфимуму их мультсет-факторизаций: factorMultiset(gcd(m,n)) = factorMultiset(m) ⊓ factorMultiset(n).
LaTeX
$$$ \\operatorname{factorMultiset}(\\gcd(m,n)) = \\operatorname{factorMultiset}(m) \\inf \\operatorname{factorMultiset}(n) $$$
Lean4
/-- The gcd and lcm operations on positive integers correspond
to the inf and sup operations on multisets. -/
theorem factorMultiset_gcd (m n : ℕ+) : factorMultiset (gcd m n) = factorMultiset m ⊓ factorMultiset n :=
by
apply le_antisymm
· apply le_inf_iff.mpr; constructor <;> apply factorMultiset_le_iff.mpr
· exact gcd_dvd_left m n
· exact gcd_dvd_right m n
· rw [← PrimeMultiset.prod_dvd_iff, prod_factorMultiset]
apply dvd_gcd <;> rw [PrimeMultiset.prod_dvd_iff']
· exact inf_le_left
· exact inf_le_right
