English
Let a, b be positive integers. Then for every prime p, the exponent of p in the prime factorization of a ⟂ lcm(a, b) equals the maximum of the exponents of p in a and in b.
Русский
Пусть a, b — положительные целые. Тогда для каждого простого p показатель p в факторизации НОК(a, b) равен максимуму показателей в a и в b.
LaTeX
$$$ (a \mathrm{lcm} b).factorization = a.factorization \sqcup b.factorization $$$
Lean4
theorem factorization_lcm {a b : ℕ} (ha : a ≠ 0) (hb : b ≠ 0) :
(a.lcm b).factorization = a.factorization ⊔ b.factorization :=
by
rw [← add_right_inj (a.gcd b).factorization, ←
factorization_mul (mt gcd_eq_zero_iff.1 fun h => ha h.1) (lcm_ne_zero ha hb), gcd_mul_lcm, factorization_gcd ha hb,
factorization_mul ha hb]
ext1
exact (min_add_max _ _).symm
