From 73922b54f46f4e76fd09d1353a273c84bc87526b Mon Sep 17 00:00:00 2001
From: Ruben-VandeVelde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Date: Wed, 17 Mar 2021 16:20:30 +0000
Subject: [PATCH] feat(data/zsqrtd/basic): add some lemmas about conj, norm
 (#6715)

---
 src/data/zsqrtd/basic.lean | 48 +++++++++++++++++++++++++++++++-------
 1 file changed, 40 insertions(+), 8 deletions(-)

diff --git a/src/data/zsqrtd/basic.lean b/src/data/zsqrtd/basic.lean
index ed665d6706734..47e675b88e774 100644
--- a/src/data/zsqrtd/basic.lean
+++ b/src/data/zsqrtd/basic.lean
@@ -77,14 +77,6 @@ instance : has_neg ℤ√d := ⟨zsqrtd.neg⟩
 @[simp] theorem neg_im : ∀ z : ℤ√d, (-z).im = -z.im
 | ⟨x, y⟩ := rfl
 
-/-- Conjugation in `ℤ√d`. The conjugate of `a + b √d` is `a - b √d`. -/
-def conj : ℤ√d → ℤ√d
-| ⟨x, y⟩ := ⟨x, -y⟩
-@[simp] theorem conj_re : ∀ z : ℤ√d, (conj z).re = z.re
-| ⟨x, y⟩ := rfl
-@[simp] theorem conj_im : ∀ z : ℤ√d, (conj z).im = -z.im
-| ⟨x, y⟩ := rfl
-
 /-- Multiplication in `ℤ√d` -/
 def mul : ℤ√d → ℤ√d → ℤ√d
 | ⟨x, y⟩ ⟨x', y'⟩ := ⟨x * x' + d * y * y', x * y' + y * x'⟩
@@ -116,6 +108,39 @@ instance : semiring ℤ√d           := by apply_instance
 instance : ring ℤ√d               := by apply_instance
 instance : distrib ℤ√d            := by apply_instance
 
+/-- Conjugation in `ℤ√d`. The conjugate of `a + b √d` is `a - b √d`. -/
+def conj : ℤ√d → ℤ√d
+| ⟨x, y⟩ := ⟨x, -y⟩
+@[simp] theorem conj_re : ∀ z : ℤ√d, (conj z).re = z.re
+| ⟨x, y⟩ := rfl
+@[simp] theorem conj_im : ∀ z : ℤ√d, (conj z).im = -z.im
+| ⟨x, y⟩ := rfl
+
+/-- `conj` as an `add_monoid_hom`. -/
+def conj_hom : ℤ√d →+ ℤ√d :=
+{ to_fun := conj,
+  map_add' := λ ⟨a, ai⟩ ⟨b, bi⟩, ext.mpr ⟨rfl, neg_add _ _⟩,
+  map_zero' := ext.mpr ⟨rfl, neg_zero⟩ }
+
+@[simp] lemma conj_zero : conj (0 : ℤ√d) = 0 :=
+conj_hom.map_zero
+
+@[simp] lemma conj_one : conj (1 : ℤ√d) = 1 :=
+by simp only [zsqrtd.ext, zsqrtd.conj_re, zsqrtd.conj_im, zsqrtd.one_im, neg_zero, eq_self_iff_true,
+  and_self]
+
+@[simp] lemma conj_neg (x : ℤ√d) : (-x).conj = -x.conj :=
+conj_hom.map_neg x
+
+@[simp] lemma conj_add (x y : ℤ√d) : (x + y).conj = x.conj + y.conj :=
+conj_hom.map_add x y
+
+@[simp] lemma conj_sub (x y : ℤ√d) : (x - y).conj = x.conj - y.conj :=
+conj_hom.map_sub x y
+
+@[simp] lemma conj_conj {d : ℤ} (x : ℤ√d) : x.conj.conj = x :=
+by simp only [ext, true_and, conj_re, eq_self_iff_true, neg_neg, conj_im]
+
 instance : nontrivial ℤ√d :=
 ⟨⟨0, 1, dec_trivial⟩⟩
 
@@ -267,6 +292,13 @@ by { simp only [norm, mul_im, mul_re], ring }
 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]
 
+@[simp] lemma norm_neg (x : ℤ√d) : (-x).norm = x.norm :=
+coe_int_inj $ by simp only [norm_eq_mul_conj, conj_neg, neg_mul_eq_neg_mul_symm,
+  mul_neg_eq_neg_mul_symm, neg_neg]
+
+@[simp] lemma norm_conj (x : ℤ√d) : x.conj.norm = x.norm :=
+coe_int_inj $ by simp only [norm_eq_mul_conj, conj_conj, mul_comm]
+
 instance : is_monoid_hom norm :=
 { map_one := norm_one, map_mul := norm_mul }