rw [UniqueFactorizationMonoid.normalizedFactors_pow, Multiset.filter_nsmul]
z : ℤ
n : ℕ
⊢ Multiset.filter Odd (UniqueFactorizationMonoid.normalizedFactors (z ^ n)) =
    n • Multiset.filter Odd (UniqueFactorizationMonoid.normalizedFactors z)
no goals