disjoint_primeFactors — Mathlib

English

If a and b are Coprime, then a.primeFactors and b.primeFactors are disjoint.

Русский

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

LaTeX

$$$ \\mathrm{Coprime}(a,b) \\Rightarrow Disjoint a.primeFactors b.primeFactors $$$

Lean4

protected theorem disjoint_primeFactors (hab : Coprime a b) : Disjoint a.primeFactors b.primeFactors :=
  List.disjoint_toFinset_iff_disjoint.2 <| coprime_primeFactorsList_disjoint hab

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