disjoint_primeFactors — Mathlib

English

Coprime elements have disjoint normalized factors; the statement is accessed via a deprecated alias.

Русский

Взаимно простые элементы имеют непересекающиеся нормализованные факторы; формулировка устарела.

LaTeX

$$Deprecated$$

Lean4

/-- Coprime elements have disjoint prime factors (as finsets). -/
@[deprecated "UniqueFactorizationMonoid.disjoint_primeFactors, IsCoprime.isRelPrime" (since := "2025-05-31")]
theorem disjoint_primeFactors (hc : IsCoprime a b) : Disjoint (primeFactors a) (primeFactors b) :=
  UniqueFactorizationMonoid.disjoint_primeFactors hc.isRelPrime

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