disjoint_primeFactors — Mathlib

English

For all a,b ≠ 0, Disjoint a.primeFactors b.primeFactors is equivalent to Coprime a b.

Русский

Для всех a,b ≠ 0 множество простых делителей a и b не пересекаются тогда и только тогда, когда a и b взаимно просты.

LaTeX

$$$ (a \\neq 0) \\land (b \\neq 0) \\Rightarrow Disjoint a.primeFactors b.primeFactors \\Leftrightarrow Coprime a b $$$

Lean4

@[simp]
theorem disjoint_primeFactors (ha : a ≠ 0) (hb : b ≠ 0) : Disjoint a.primeFactors b.primeFactors ↔ Coprime a b := by
  simp [disjoint_iff_inter_eq_empty, coprime_iff_gcd_eq_one, ← primeFactors_gcd, ha, hb]

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