English
Let M be a cancellative commutative monoid with zero that is a unique factorization monoid. Then the multiset of prime factors of radical(a) equals the multiset of prime factors of a; i.e. primeFactors(radical(a)) = primeFactors(a).
Русский
Пусть M — коммутативное моноид с нулём без нулевых делителей, имеющее единственную факторизацию. Тогда множестeвo простых делителей радикала элемента a совпадает с множeством простых делителей самого a: primeFactors(radical(a)) = primeFactors(a).
LaTeX
$$$\operatorname{primeFactors}(\operatorname{radical}(a)) = \operatorname{primeFactors}(a)$$$
Lean4
@[simp]
theorem primeFactors_radical : primeFactors (radical a) = primeFactors a :=
by
obtain rfl | ha₀ := eq_or_ne a 0
· simp [primeFactors]
have : Nontrivial M := ⟨a, 0, ha₀⟩
ext p
simp +contextual [mem_primeFactors, mem_normalizedFactors_iff', dvd_radical_iff_of_irreducible, ha₀]
