rw [isUnit_iff_dvd_one] at this
case intro
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
heven : Even (Zsqrtd.norm a)
this✝ : Even a.re ↔ Even a.im
hre : 2 ∣ a.re
him : 2 ∣ a.im
this : IsUnit 2
⊢ False
case intro
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
heven : Even (Zsqrtd.norm a)
this✝ : Even a.re ↔ Even a.im
hre : 2 ∣ a.re
him : 2 ∣ a.im
this : 2 ∣ 1
⊢ False