exact associated'_of_abs_eq hre him
case intro
x y : ℤ√(-3)
h : Associated (Zsqrtd.norm x) (Zsqrtd.norm y)
hx : IsCoprime x.re x.im
hy : IsCoprime y.re y.im
h' : OddPrimeOrFour (Zsqrtd.norm x)
heq : Zsqrtd.norm x = Zsqrtd.norm y
hre : abs x.re = abs y.re
him : abs x.im = abs y.im
⊢ Associated' x y
no goals