English
Let M be a cancellative commutative monoid with zero, normalization, and a unique factorization monoid. For every a ∈ M and every n ∈ ℕ with n ≠ 0, the set of prime factors of a^n equals the set of prime factors of a.
Русский
Пусть M — коммутативный моноид с нулём, удовлетворяющий условиямCancelCommMonoidWithZero, NormalizationMonoid и UniqueFactorizationMonoid. Для любого a ∈ M и любого n ∈ ℕ, не равного нулю, множество простых делителей a^n совпадает с множеством простых делителей a.
LaTeX
$$$ n \neq 0 \Rightarrow \operatorname{primeFactors}(a^n) = \operatorname{primeFactors}(a) $$$
Lean4
theorem primeFactors_pow (a : M) {n : ℕ} (hn : n ≠ 0) : primeFactors (a ^ n) = primeFactors a := by
simp_rw [primeFactors, normalizedFactors_pow, Multiset.toFinset_nsmul _ _ hn]
