English
For hd : d < 0 and z ∈ Z√d, z.norm = 0 iff z = 0.
Русский
Если $d < 0$ и $z \\in \\mathbb{Z}[\\sqrt{d}]$, то $\\|z\\| = 0$ тогда и только тогда, когда $z = 0$.
LaTeX
$${d : Int} (hd : d < 0) (z : ℤ√d) : z.norm = 0 ↔ z = 0$$
Lean4
theorem norm_eq_zero_iff {d : ℤ} (hd : d < 0) (z : ℤ√d) : z.norm = 0 ↔ z = 0 :=
by
constructor
· intro h
rw [norm_def, sub_eq_add_neg, mul_assoc] at h
have left := mul_self_nonneg z.re
have right := neg_nonneg.mpr (mul_nonpos_of_nonpos_of_nonneg hd.le (mul_self_nonneg z.im))
obtain ⟨ha, hb⟩ := (add_eq_zero_iff_of_nonneg left right).mp h
ext <;> apply eq_zero_of_mul_self_eq_zero
· exact ha
· rw [neg_eq_zero, mul_eq_zero] at hb
exact hb.resolve_left hd.ne
· rintro rfl
exact norm_zero
