rw [hnorm]
case h
a b c : ℤ√(-3)
h : IsCoprime a.re a.im
hbmem : b ∈ factorization' h
hcmem : c ∈ factorization' h
hnorm : Zsqrtd.norm b = Zsqrtd.norm c
⊢ Associated (Zsqrtd.norm b) (Zsqrtd.norm c)
no goals