case intro
d✝ d : ℤ
hd : d ≤ 0
x : ℤ√d
u : (ℤ√d)ˣ
⊢ norm x = norm (x * ↑u)
d✝ d : ℤ
hd : d ≤ 0
x y : ℤ√d
h : Associated x y
⊢ norm x = norm y
obtain ⟨u, rfl⟩ := h
no goals
case intro
d✝ d : ℤ
hd : d ≤ 0
x : ℤ√d
u : (ℤ√d)ˣ
⊢ norm x = norm (x * ↑u)
rw [norm_mul, (norm_eq_one_iff' hd _).mpr u.isUnit, mul_one]