rfl
case intro.inr
a b : ℤ√(-3)
h : IsCoprime a.re a.im
f : Multiset (ℤ√(-3)) := factorization' h
hmem : b ∈ f
h1 : a = -Multiset.prod f
⊢ Multiset.prod (factorization' h) ∣ Multiset.prod (factorization' h)
no goals