radical_dvd_radical_iff_primeFactors_subset_primeFactors

English

For any a,b, radical(a) divides radical(b) if and only if primeFactors(a) is a subset of primeFactors(b).

Русский

Для любых a,b радикал(a) делится радикалом(b) тогда и только тогда, когда primeFactors(a) включены в primeFactors(b).

LaTeX

$$$\operatorname{radical}(a) \mid \operatorname{radical}(b) \iff \operatorname{primeFactors}(a) \subseteq \operatorname{primeFactors}(b)$$$

Lean4

theorem radical_dvd_radical_iff_primeFactors_subset_primeFactors :
    radical a ∣ radical b ↔ primeFactors a ⊆ primeFactors b := by
  classical
    rw [radical_dvd_radical_iff_normalizedFactors_subset_normalizedFactors, primeFactors, primeFactors,
    Multiset.toFinset_subset]

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