simp only [evenFactorExp, Multiset.count_eq_zero, hn]
case h.e'_3
n : ℕ
ih : ∀ m < n, ∀ {a : ℤ√(-3)}, IsCoprime a.re a.im → a.norm.natAbs = m → Even (evenFactorExp m)
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hn : a.norm.natAbs = n
hparity : ¬Even a.norm.natAbs
⊢ evenFactorExp n = 0
case h.e'_3
n : ℕ
ih : ∀ m < n, ∀ {a : ℤ√(-3)}, IsCoprime a.re a.im → a.norm.natAbs = m → Even (evenFactorExp m)
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hn : a.norm.natAbs = n
hparity : ¬Even a.norm.natAbs
⊢ 2 ∉ UniqueFactorizationMonoid.normalizedFactors n