rw [Zsqrtd.norm_mul]
case intro
d : ℤ
f : ℤ√d
u : (ℤ√d)ˣ
this : IsUnit (norm ↑u)
⊢ Associated (norm f) (norm (f * ↑u))
case intro
d : ℤ
f : ℤ√d
u : (ℤ√d)ˣ
this : IsUnit (norm ↑u)
⊢ Associated (norm f) (norm f * norm ↑u)