disjoint_primeFactors — Mathlib

English

Relatively prime elements have disjoint prime factors (as finite sets).

Русский

Относительно простые элементы имеют непересекающиеся множества простых делителей.

LaTeX

$$$ IsRelPrime(a,b) \Rightarrow Disjoint(\operatorname{primeFactors}(a), \operatorname{primeFactors}(b)) $$$

Lean4

/-- Relatively prime elements have disjoint prime factors (as finsets). -/
theorem disjoint_primeFactors (hc : IsRelPrime a b) : Disjoint (primeFactors a) (primeFactors b) := by
  classical exact Multiset.disjoint_toFinset.mpr (disjoint_normalizedFactors hc)

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