disjoint_normalizedFactors — Mathlib

English

For any a,b with b ≠ 0, radical(a) divides b if and only if primeFactors(a) ⊆ primeFactors(b).

Русский

Для любых a,b с b ≠ 0: radical(a) делит b тогда и только тогда, когда primeFactors(a) ⊆ primeFactors(b).

LaTeX

$$$\operatorname{radical}(a) \mid b \iff \operatorname{primeFactors}(a) \subseteq \operatorname{primeFactors}(b) \quad (hb:\, b \neq 0)$$$

Lean4

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

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