refactor(number_theory/zsqrtd): replace zsqrtd.conj with star (#18572)

eric-wieser · eric-wieser · commit 2af0836443b4 · 2023-03-12T20:39:34.000Z
This allows more existing lemmas to be used; notably, `unitary (zqsrt d)` becomes something we can talk about.
diff --git a/src/number_theory/pell_matiyasevic.lean b/src/number_theory/pell_matiyasevic.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
 
+import algebra.star.unitary
 import data.nat.modeq
 import number_theory.zsqrtd.basic
 
@@ -121,15 +122,18 @@ theorem is_pell_nat {x y : ℕ} : is_pell ⟨x, y⟩ ↔ x*x - d*y*y = 1 :=
 λh, show ((x*x : ℕ) - (d*y*y:ℕ) : ℤ) = 1,
   by rw [← int.coe_nat_sub $ le_of_lt $ nat.lt_of_sub_eq_succ h, h]; refl⟩
 
-theorem is_pell_norm : Π {b : ℤ√d}, is_pell b ↔ b * b.conj = 1
+theorem is_pell_norm : Π {b : ℤ√d}, is_pell b ↔ b * star b = 1
 | ⟨x, y⟩ := by simp [zsqrtd.ext, is_pell, mul_comm]; ring_nf
 
+theorem is_pell_iff_mem_unitary : Π {b : ℤ√d}, is_pell b ↔ b ∈ unitary ℤ√d
+| ⟨x, y⟩ := by rw [unitary.mem_iff, is_pell_norm, mul_comm (star _), and_self]
+
 theorem is_pell_mul {b c : ℤ√d} (hb : is_pell b) (hc : is_pell c) : is_pell (b * c) :=
 is_pell_norm.2 (by simp [mul_comm, mul_left_comm,
-  zsqrtd.conj_mul, pell.is_pell_norm.1 hb, pell.is_pell_norm.1 hc])
+  star_mul, pell.is_pell_norm.1 hb, pell.is_pell_norm.1 hc])
 
-theorem is_pell_conj : ∀ {b : ℤ√d}, is_pell b ↔ is_pell b.conj | ⟨x, y⟩ :=
-by simp [is_pell, zsqrtd.conj]
+theorem is_pell_star : ∀ {b : ℤ√d}, is_pell b ↔ is_pell (star b) | ⟨x, y⟩ :=
+by simp [is_pell, zsqrtd.star_mk]
 
 @[simp] theorem pell_zd_succ (n : ℕ) : pell_zd (n+1) = pell_zd n * ⟨a, 1⟩ :=
 by simp [zsqrtd.ext]
@@ -187,7 +191,7 @@ lemma eq_pell_lem : ∀n (b:ℤ√d), 1 ≤ b → is_pell b → b ≤ pell_zd n
   if ha : (⟨↑a, 1⟩ : ℤ√d) ≤ b then
     let ⟨m, e⟩ := eq_pell_lem n (b * ⟨a, -1⟩)
       (by rw ← a1m; exact mul_le_mul_of_nonneg_right ha am1p)
-      (is_pell_mul hp (is_pell_conj.1 is_pell_one))
+      (is_pell_mul hp (is_pell_star.1 is_pell_one))
       (by have t := mul_le_mul_of_nonneg_right h am1p;
         rwa [pell_zd_succ, mul_assoc, a1m, mul_one] at t) in
     ⟨m+1, by rw [show b = b * ⟨a, -1⟩ * ⟨a, 1⟩, by rw [mul_assoc, eq.trans (mul_comm _ _) a1m];
@@ -245,7 +249,7 @@ by injection (pell_zd_add _ m n) with _ h;
     repeat {rw ← int.coe_nat_add at h <|> rw ← int.coe_nat_mul at h};
     exact int.coe_nat_inj h
 
-theorem pell_zd_sub {m n} (h : n ≤ m) : pell_zd (m - n) = pell_zd m * (pell_zd n).conj :=
+theorem pell_zd_sub {m n} (h : n ≤ m) : pell_zd (m - n) = pell_zd m * star (pell_zd n) :=
 let t := pell_zd_add n (m - n) in
 by rw [add_tsub_cancel_of_le h] at t;
     rw [t, mul_comm (pell_zd _ n) _, mul_assoc, (is_pell_norm _).1 (is_pell_pell_zd _ _), mul_one]
diff --git a/src/number_theory/zsqrtd/basic.lean b/src/number_theory/zsqrtd/basic.lean
@@ -122,33 +122,16 @@ 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 (z : ℤ√d) : ℤ√d := ⟨z.1, -z.2⟩
-@[simp] lemma conj_re (z : ℤ√d) : (conj z).re = z.re := rfl
-@[simp] lemma conj_im (z : ℤ√d) : (conj z).im = -z.im := rfl
+instance : has_star ℤ√d :=
+{ star := λ z, ⟨z.1, -z.2⟩ }
+@[simp] lemma star_mk (x y : ℤ) : star (⟨x, y⟩ : ℤ√d) = ⟨x, -y⟩ := rfl
+@[simp] lemma star_re (z : ℤ√d) : (star z).re = z.re := rfl
+@[simp] lemma star_im (z : ℤ√d) : (star z).im = -z.im := 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 := rfl
-
-@[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 : star_ring ℤ√d :=
+{ star_involutive := λ x, ext.mpr ⟨rfl, neg_neg _⟩,
+  star_mul := λ a b, ext.mpr ⟨by simp; ring, by simp; ring⟩,
+  star_add := λ a b, ext.mpr ⟨rfl, neg_add _ _⟩ }
 
 instance : nontrivial ℤ√d :=
 ⟨⟨0, 1, dec_trivial⟩⟩
@@ -188,12 +171,9 @@ by simp [ext]
 theorem decompose {x y : ℤ} : (⟨x, y⟩ : ℤ√d) = x + sqrtd * y :=
 by simp [ext]
 
-theorem mul_conj {x y : ℤ} : (⟨x, y⟩ * conj ⟨x, y⟩ : ℤ√d) = x * x - d * y * y :=
+theorem mul_star {x y : ℤ} : (⟨x, y⟩ * star ⟨x, y⟩ : ℤ√d) = x * x - d * y * y :=
 by simp [ext, sub_eq_add_neg, mul_comm]
 
-theorem conj_mul {a b : ℤ√d} : conj (a * b) = conj a * conj b :=
-by { simp [ext], ring }
-
 protected lemma coe_int_add (m n : ℤ) : (↑(m + n) : ℤ√d) = ↑m + ↑n :=
 (int.cast_ring_hom _).map_add _ _
 protected lemma coe_int_sub (m n : ℤ) : (↑(m - n) : ℤ√d) = ↑m - ↑n :=
@@ -376,15 +356,15 @@ def norm_monoid_hom : ℤ√d →* ℤ :=
   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]
+lemma norm_eq_mul_conj (n : ℤ√d) : (norm n : ℤ√d) = n * star n :=
+by cases n; simp [norm, star, 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,
+coe_int_inj $ by simp only [norm_eq_mul_conj, star_neg, neg_mul,
   mul_neg, 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]
+@[simp] lemma norm_conj (x : ℤ√d) : (star x).norm = x.norm :=
+coe_int_inj $ by simp only [norm_eq_mul_conj, star_star, mul_comm]
 
 lemma norm_nonneg (hd : d ≤ 0) (n : ℤ√d) : 0 ≤ n.norm :=
 add_nonneg (mul_self_nonneg _)
@@ -394,10 +374,10 @@ add_nonneg (mul_self_nonneg _)
 lemma norm_eq_one_iff {x : ℤ√d} : x.norm.nat_abs = 1 ↔ is_unit x :=
 ⟨λ h, is_unit_iff_dvd_one.2 $
   (le_total 0 (norm x)).cases_on
-    (λ hx, show x ∣ 1, from ⟨x.conj,
+    (λ hx, show x ∣ 1, from ⟨star x,
       by rwa [← int.coe_nat_inj', int.nat_abs_of_nonneg hx,
         ← @int.cast_inj (ℤ√d) _ _, norm_eq_mul_conj, eq_comm] at h⟩)
-    (λ hx, show x ∣ 1, from ⟨- x.conj,
+    (λ hx, show x ∣ 1, from ⟨- star x,
       by rwa [← int.coe_nat_inj', int.of_nat_nat_abs_of_nonpos hx,
         ← @int.cast_inj (ℤ√d) _ _, int.cast_neg, norm_eq_mul_conj, neg_mul_eq_mul_neg,
         eq_comm] at h⟩),
diff --git a/src/number_theory/zsqrtd/gaussian_int.lean b/src/number_theory/zsqrtd/gaussian_int.lean
@@ -36,6 +36,7 @@ and definitions about `zsqrtd` can easily be used.
 -/
 
 open zsqrtd complex
+open_locale complex_conjugate
 
 /-- The Gaussian integers, defined as `ℤ√(-1)`. -/
 @[reducible] def gaussian_int : Type := zsqrtd (-1)
@@ -75,6 +76,11 @@ by apply complex.ext; simp [to_complex_def]
 @[simp] lemma to_complex_zero : ((0 : ℤ[i]) : ℂ) = 0 := to_complex.map_zero
 @[simp] lemma to_complex_neg (x : ℤ[i]) : ((-x : ℤ[i]) : ℂ) = -x := to_complex.map_neg _
 @[simp] lemma to_complex_sub (x y : ℤ[i]) : ((x - y : ℤ[i]) : ℂ) = x - y := to_complex.map_sub _ _
+@[simp] lemma to_complex_star (x : ℤ[i]) : ((star x : ℤ[i]) : ℂ) = conj (x : ℂ) :=
+begin
+  rw [to_complex_def₂, to_complex_def₂],
+  exact congr_arg2 _ rfl (int.cast_neg _),
+end
 
 @[simp] lemma to_complex_inj {x y : ℤ[i]} : (x : ℂ) = y ↔ x = y :=
 by cases x; cases y; simp [to_complex_def₂]
@@ -108,11 +114,11 @@ lemma nat_abs_norm_eq (x : ℤ[i]) : x.norm.nat_abs =
 int.coe_nat_inj $ begin simp, simp [zsqrtd.norm] end
 
 instance : has_div ℤ[i] :=
-⟨λ x y, let n := (norm y : ℚ)⁻¹, c := y.conj in
+⟨λ x y, let n := (norm y : ℚ)⁻¹, c := star y in
   ⟨round ((x * c).re * n : ℚ), round ((x * c).im * n : ℚ)⟩⟩
 
-lemma div_def (x y : ℤ[i]) : x / y = ⟨round ((x * conj y).re / norm y : ℚ),
-  round ((x * conj y).im / norm y : ℚ)⟩ :=
+lemma div_def (x y : ℤ[i]) : x / y = ⟨round ((x * star y).re / norm y : ℚ),
+  round ((x * star y).im / norm y : ℚ)⟩ :=
 show zsqrtd.mk _ _ = _, by simp [div_eq_mul_inv]
 
 lemma to_complex_div_re (x y : ℤ[i]) : ((x / y : ℤ[i]) : ℂ).re = round ((x / y : ℂ).re) :=
