mul_primeFactors_disjUnion — Mathlib

English

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

Русский

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

LaTeX

$$Deprecated$$

Lean4

@[deprecated "UniqueFactorizationMonoid.primeFactors_mul_eq_disjUnion, IsCoprime.isRelPrime" (since := "2025-05-31")]
theorem mul_primeFactors_disjUnion (hc : IsCoprime a b) :
    primeFactors (a * b) = (primeFactors a).disjUnion (primeFactors b) (disjoint_primeFactors hc) :=
  UniqueFactorizationMonoid.primeFactors_mul_eq_disjUnion hc.isRelPrime

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