coprime_factorizationLCMLeft_factorizationLCMRight

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']

Похожие утверждения