English
For every n, normalizedFactors n equals the multiset of prime factors of n (primeFactorsList).
Русский
Для каждого числа n нормализованные множества факторов совпадают с множеством простых факторов n.
LaTeX
$$normalizedFactors(n) = Multiset.ofList(n.primeFactorsList)$$
Lean4
theorem factors_eq : ∀ n : ℕ, normalizedFactors n = n.primeFactorsList
| 0 => by simp
| n + 1 => by
rw [← Multiset.rel_eq, ← associated_eq_eq]
apply UniqueFactorizationMonoid.factors_unique irreducible_of_normalized_factor _
· rw [Multiset.prod_coe, Nat.prod_primeFactorsList n.succ_ne_zero]
exact prod_normalizedFactors n.succ_ne_zero
· intro x hx
rw [Nat.irreducible_iff_prime, ← Nat.prime_iff]
exact Nat.prime_of_mem_primeFactorsList hx
