rw [Zsqrtd.norm_mul, Zsqrtd.norm_conj]
case intro.inr
p : ℤ√(-3)
hpprime : Prime (Zsqrtd.norm p)
u : ℤ√(-3)
hdvd : Zsqrtd.norm p ∣ Zsqrtd.norm (star p * u)
⊢ Zsqrtd.norm (star p * u) = Zsqrtd.norm p * Zsqrtd.norm u
no goals