coprime_primeFactorsList_disjoint

English

If a and b are coprime, their prime factor lists are disjoint.

Русский

Если a и b взаимно просты, их списки простых делителей не пересекаются.

LaTeX

$$hab : a.Coprime b → List.Disjoint a.primeFactorsList b.primeFactorsList$$

Lean4

/-- The sets of factors of coprime `a` and `b` are disjoint -/
theorem coprime_primeFactorsList_disjoint {a b : ℕ} (hab : a.Coprime b) :
    List.Disjoint a.primeFactorsList b.primeFactorsList :=
  by
  intro q hqa hqb
  apply not_prime_one
  rw [← eq_one_of_dvd_coprimes hab (dvd_of_mem_primeFactorsList hqa) (dvd_of_mem_primeFactorsList hqb)]
  exact prime_of_mem_primeFactorsList hqa

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