English
Let d be an integer which is not a square. Then for every element a in the quadratic ring Z[√d], the norm of a vanishes if and only if a is the zero element.
Русский
Пусть d целое число, которое не является квадратом. Тогда для каждого элемента a из кольца Z[√d] норма a равна нулю тогда и только тогда, когда a = 0.
LaTeX
$$$ (\\forall d \\in \\mathbb{Z})\\,(\\operatorname{Nonsquare}(d) \\Rightarrow (\\forall a \\in \\mathbb{Z}[\\sqrt{d}],\\ \\operatorname{norm}(a) = 0 \\iff a = 0))). $$$
Lean4
theorem norm_eq_zero {d : ℤ} (h_nonsquare : ∀ n : ℤ, d ≠ n * n) (a : ℤ√d) : norm a = 0 ↔ a = 0 :=
by
refine ⟨fun ha => Zsqrtd.ext_iff.mpr ?_, fun h => by rw [h, norm_zero]⟩
dsimp only [norm] at ha
rw [sub_eq_zero] at ha
by_cases h : 0 ≤ d
· obtain ⟨d', rfl⟩ := Int.eq_ofNat_of_zero_le h
haveI : Nonsquare d' := ⟨fun n h => h_nonsquare n <| mod_cast h⟩
exact divides_sq_eq_zero_z ha
· push_neg at h
suffices a.re * a.re = 0 by
rw [eq_zero_of_mul_self_eq_zero this] at ha ⊢
simpa only [true_and, or_self_right, re_zero, im_zero, eq_self_iff_true, zero_eq_mul, mul_zero, mul_eq_zero, h.ne,
false_or, or_self_iff] using ha
apply _root_.le_antisymm _ (mul_self_nonneg _)
rw [ha, mul_assoc]
exact mul_nonpos_of_nonpos_of_nonneg h.le (mul_self_nonneg _)
