radical_dvd_radical_iff_normalizedFactors_subset_normalizedFactors

English

For all a,b, radical(a) divides radical(b) if and only if normalizedFactors(a) is a subset of normalizedFactors(b).

Русский

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

LaTeX

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

Lean4

theorem radical_dvd_radical_iff_normalizedFactors_subset_normalizedFactors :
    radical a ∣ radical b ↔ normalizedFactors a ⊆ normalizedFactors b :=
  by
  obtain rfl | ha₀ := eq_or_ne a 0
  · simp
  have : Nontrivial M := ⟨a, 0, ha₀⟩
  rw [dvd_iff_normalizedFactors_le_normalizedFactors radical_ne_zero radical_ne_zero,
    Multiset.le_iff_subset (normalizedFactors_nodup isRadical_radical)]
  simp only [Multiset.subset_iff, ← mem_primeFactors, primeFactors_radical]

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