radical_dvd_iff_primeFactors_subset

English

For any a,b with b ≠ 0, radical(a) divides b iff 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

theorem radical_dvd_iff_primeFactors_subset (hb : b ≠ 0) : radical a ∣ b ↔ primeFactors a ⊆ primeFactors b := by
  rw [← dvd_radical_iff isRadical_radical hb, radical_dvd_radical_iff_primeFactors_subset_primeFactors]

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