simp only [oddFactors]
z n : ℕ
⊢ oddFactors (z ^ n) = n • oddFactors z
z n : ℕ
⊢ Multiset.filter Odd (UniqueFactorizationMonoid.normalizedFactors (z ^ n)) =
    n • Multiset.filter Odd (UniqueFactorizationMonoid.normalizedFactors z)