English
The left and right parts of the LCM factorization are coprime.
Русский
Левая и правая части факторизации НОК взаимно просты.
LaTeX
$$$(\text{factorizationLCMLeft }a b) \; \text{Coprime} \; (\text{factorizationLCMRight }a b).$$$
Lean4
theorem coprime_factorizationLCMLeft_factorizationLCMRight :
(factorizationLCMLeft a b).Coprime (factorizationLCMRight a b) :=
by
rw [factorizationLCMLeft, factorizationLCMRight]
refine coprime_prod_left_iff.mpr fun p hp ↦ coprime_prod_right_iff.mpr fun q hq ↦ ?_
dsimp only; split_ifs with h h'
any_goals simp only [coprime_one_right_eq_true, coprime_one_left_eq_true]
refine coprime_pow_primes _ _ (prime_of_mem_primeFactors hp) (prime_of_mem_primeFactors hq) ?_
contrapose! h'; rwa [← h']