zero_notMem_normalizedFactors — Mathlib

English

If a and b are relatively prime (IsRelPrime), then the multisets of their normalized factors are disjoint.

Русский

Если a и b относительно просты (IsRelPrime), то их множества нормализованных факторов не пересекаются.

LaTeX

$$IsRelPrime(a,b) \rightarrow \operatorname{Disjoint}(\operatorname{normalizedFactors}(a), \operatorname{normalizedFactors}(b))$$

Lean4

theorem zero_notMem_normalizedFactors (x : α) : (0 : α) ∉ normalizedFactors x := fun h =>
  Prime.ne_zero (prime_of_normalized_factor _ h) rfl

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