disjoint_divisors_filter_isPrimePow

English

If a and b are coprime, then the sets a.divisors.filter IsPrimePow and b.divisors.filter IsPrimePow are disjoint.

Русский

Если a и b взаимно просты, то множества a.divisors.filter IsPrimePow и b.divisors.filter IsPrimePow взаимно дизъйнты.

LaTeX

$$$\mathrm{Disjoint} (a.divisors.filter IsPrimePow) (b.divisors.filter IsPrimePow).$$$

Lean4

theorem disjoint_divisors_filter_isPrimePow {a b : ℕ} (hab : a.Coprime b) :
    Disjoint (a.divisors.filter IsPrimePow) (b.divisors.filter IsPrimePow) :=
  by
  simp only [Finset.disjoint_left, Finset.mem_filter, and_imp, Nat.mem_divisors, not_and]
  rintro n han _ha hn hbn _hb -
  exact hn.ne_one (Nat.eq_one_of_dvd_coprimes hab han hbn)

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