feat(data/zsqrtd/basic): add some lemmas about norm (#7114)

src/data/zsqrtd/basic.lean

@@ -277,6 +277,7 @@ cast nonnegg_comm (nonnegg_cases_right h)
 section norm
 
 def norm (n : ℤ√d) : ℤ := n.re * n.re - d * n.im * n.im
+lemma norm_def (n : ℤ√d) : n.norm = n.re * n.re - d * n.im * n.im := rfl
 
 @[simp] lemma norm_zero : norm 0 = 0 := by simp [norm]
 
@@ -289,6 +290,12 @@ def norm (n : ℤ√d) : ℤ := n.re * n.re - d * n.im * n.im
 @[simp] lemma norm_mul (n m : ℤ√d) : norm (n * m) = norm n * norm m :=
 by { simp only [norm, mul_im, mul_re], ring }
 
+/-- `norm` as a `monoid_hom`. -/
+def norm_monoid_hom : ℤ√d →* ℤ :=
+{ to_fun := norm,
+  map_mul' := norm_mul,
+  map_one' := norm_one }
+
 lemma norm_eq_mul_conj (n : ℤ√d) : (norm n : ℤ√d) = n * n.conj :=
 by cases n; simp [norm, conj, zsqrtd.ext, mul_comm, sub_eq_add_neg]
 
@@ -324,6 +331,36 @@ lemma norm_eq_one_iff {x : ℤ√d} : x.norm.nat_abs = 1 ↔ is_unit x :=
   exact this.1
 end⟩
 
+lemma is_unit_iff_norm_is_unit {d : ℤ} (z : ℤ√d) : is_unit z ↔ is_unit z.norm :=
+by rw [int.is_unit_iff_nat_abs_eq, norm_eq_one_iff]
+
+lemma norm_eq_one_iff' {d : ℤ} (hd : d ≤ 0) (z : ℤ√d) : z.norm = 1 ↔ is_unit z :=
+by rw [←norm_eq_one_iff, ←int.coe_nat_inj', int.nat_abs_of_nonneg (norm_nonneg hd z),
+  int.coe_nat_one]
+
+lemma norm_eq_zero_iff {d : ℤ} (hd : d < 0) (z : ℤ√d) : z.norm = 0 ↔ z = 0 :=
+begin
+  split,
+  { intro h,
+    rw [ext, zero_re, zero_im],
+    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_eq_zero_of_nonneg left right).mp h,
+    split; 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 }
+end
+
+lemma norm_eq_of_associated {d : ℤ} (hd : d ≤ 0) {x y : ℤ√d} (h : associated x y) :
+  x.norm = y.norm :=
+begin
+  obtain ⟨u, rfl⟩ := h,
+  rw [norm_mul, (norm_eq_one_iff' hd _).mpr u.is_unit, mul_one],
+end
+
 end norm
 
 end