chore(number_theory/zsqrtd/*): Missing docstrings and cleanups (#13445)

Add docstrings to `gaussian_int` and `zsqrtd.norm` and inline definitions which did not have a docstring nor deserved one.

src/number_theory/pell.lean

@@ -217,7 +217,7 @@ lemma eq_pell_lem : ∀n (b:ℤ√d), 1 ≤ b → is_pell b → b ≤ pell_zd n
 
 theorem eq_pell_zd (b : ℤ√d) (b1 : 1 ≤ b) (hp : is_pell b) : ∃n, b = pell_zd n :=
 let ⟨n, h⟩ := @zsqrtd.le_arch d b in
-eq_pell_lem n b b1 hp $ zsqrtd.le_trans h $ by rw zsqrtd.coe_nat_val; exact
+eq_pell_lem n b b1 hp $ h.trans $ by rw zsqrtd.coe_nat_val; exact
 zsqrtd.le_of_le_le
   (int.coe_nat_le_coe_nat_of_le $ le_of_lt $ n_lt_xn _ _) (int.coe_zero_le _)
 
@@ -252,11 +252,11 @@ 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]
 
 theorem xz_sub {m n} (h : n ≤ m) : xz (m - n) = xz m * xz n - d * yz m * yz n :=
-by injection (pell_zd_sub _ h) with h _; repeat {rw mul_neg at h}; exact h
+by { rw [sub_eq_add_neg, ←mul_neg], exact congr_arg zsqrtd.re (pell_zd_sub a1 h) }
 
 theorem yz_sub {m n} (h : n ≤ m) : yz (m - n) = xz n * yz m - xz m * yz n :=
-by injection (pell_zd_sub a1 h) with _ h; repeat {rw mul_neg at h};
-  rw [add_comm, mul_comm] at h; exact h
+by { rw [sub_eq_add_neg, ←mul_neg, mul_comm, add_comm],
+  exact congr_arg zsqrtd.im (pell_zd_sub a1 h) }
 
 theorem xy_coprime (n) : (xn n).coprime (yn n) :=
 nat.coprime_of_dvd' $ λk kp kx ky,

src/number_theory/zsqrtd/basic.lean

@@ -45,16 +45,14 @@ theorem of_int_re (n : ℤ) : (of_int n).re = n := rfl
 theorem of_int_im (n : ℤ) : (of_int n).im = 0 := rfl
 
 /-- The zero of the ring -/
-def zero : ℤ√d := of_int 0
-instance : has_zero ℤ√d := ⟨zsqrtd.zero⟩
+instance : has_zero ℤ√d := ⟨of_int 0⟩
 @[simp] theorem zero_re : (0 : ℤ√d).re = 0 := rfl
 @[simp] theorem zero_im : (0 : ℤ√d).im = 0 := rfl
 
 instance : inhabited ℤ√d := ⟨0⟩
 
 /-- The one of the ring -/
-def one : ℤ√d := of_int 1
-instance : has_one ℤ√d := ⟨zsqrtd.one⟩
+instance : has_one ℤ√d := ⟨of_int 1⟩
 @[simp] theorem one_re : (1 : ℤ√d).re = 1 := rfl
 @[simp] theorem one_im : (1 : ℤ√d).im = 0 := rfl
 
@@ -64,39 +62,26 @@ def sqrtd : ℤ√d := ⟨0, 1⟩
 @[simp] theorem sqrtd_im : (sqrtd : ℤ√d).im = 1 := rfl
 
 /-- Addition of elements of `ℤ√d` -/
-def add : ℤ√d → ℤ√d → ℤ√d
-| ⟨x, y⟩ ⟨x', y'⟩ := ⟨x + x', y + y'⟩
-instance : has_add ℤ√d := ⟨zsqrtd.add⟩
-@[simp] theorem add_def (x y x' y' : ℤ) :
-  (⟨x, y⟩ + ⟨x', y'⟩ : ℤ√d) = ⟨x + x', y + y'⟩ := rfl
-@[simp] theorem add_re : ∀ z w : ℤ√d, (z + w).re = z.re + w.re
-| ⟨x, y⟩ ⟨x', y'⟩ := rfl
-@[simp] theorem add_im : ∀ z w : ℤ√d, (z + w).im = z.im + w.im
-| ⟨x, y⟩ ⟨x', y'⟩ := rfl
-
-@[simp] theorem bit0_re (z) : (bit0 z : ℤ√d).re = bit0 z.re := add_re _ _
-@[simp] theorem bit0_im (z) : (bit0 z : ℤ√d).im = bit0 z.im := add_im _ _
-
-@[simp] theorem bit1_re (z) : (bit1 z : ℤ√d).re = bit1 z.re := by simp [bit1]
+instance : has_add ℤ√d := ⟨λ z w, ⟨z.1 + w.1, z.2 + w.2⟩⟩
+@[simp] lemma add_def (x y x' y' : ℤ) : (⟨x, y⟩ + ⟨x', y'⟩ : ℤ√d) = ⟨x + x', y + y'⟩ := rfl
+@[simp] lemma add_re (z w : ℤ√d) : (z + w).re = z.re + w.re := rfl
+@[simp] lemma add_im (z w : ℤ√d) : (z + w).im = z.im + w.im := rfl
+
+@[simp] lemma bit0_re (z) : (bit0 z : ℤ√d).re = bit0 z.re := rfl
+@[simp] lemma bit0_im (z) : (bit0 z : ℤ√d).im = bit0 z.im := rfl
+
+@[simp] theorem bit1_re (z) : (bit1 z : ℤ√d).re = bit1 z.re := rfl
 @[simp] theorem bit1_im (z) : (bit1 z : ℤ√d).im = bit0 z.im := by simp [bit1]
 
 /-- Negation in `ℤ√d` -/
-def neg : ℤ√d → ℤ√d
-| ⟨x, y⟩ := ⟨-x, -y⟩
-instance : has_neg ℤ√d := ⟨zsqrtd.neg⟩
-@[simp] theorem neg_re : ∀ z : ℤ√d, (-z).re = -z.re
-| ⟨x, y⟩ := rfl
-@[simp] theorem neg_im : ∀ z : ℤ√d, (-z).im = -z.im
-| ⟨x, y⟩ := rfl
+instance : has_neg ℤ√d := ⟨λ z, ⟨-z.1, -z.2⟩⟩
+@[simp] lemma neg_re (z : ℤ√d) : (-z).re = -z.re := rfl
+@[simp] lemma neg_im (z : ℤ√d) : (-z).im = -z.im := rfl
 
 /-- Multiplication in `ℤ√d` -/
-def mul : ℤ√d → ℤ√d → ℤ√d
-| ⟨x, y⟩ ⟨x', y'⟩ := ⟨x * x' + d * y * y', x * y' + y * x'⟩
-instance : has_mul ℤ√d := ⟨zsqrtd.mul⟩
-@[simp] theorem mul_re : ∀ z w : ℤ√d, (z * w).re = z.re * w.re + d * z.im * w.im
-| ⟨x, y⟩ ⟨x', y'⟩ := rfl
-@[simp] theorem mul_im : ∀ z w : ℤ√d, (z * w).im = z.re * w.im + z.im * w.re
-| ⟨x, y⟩ ⟨x', y'⟩ := rfl
+instance : has_mul ℤ√d := ⟨λ z w, ⟨z.1 * w.1 + d * z.2 * w.2, z.1 * w.2 + z.2 * w.1⟩⟩
+@[simp] lemma mul_re (z w : ℤ√d) : (z * w).re = z.re * w.re + d * z.im * w.im := rfl
+@[simp] lemma mul_im (z w : ℤ√d) : (z * w).im = z.re * w.im + z.im * w.re := rfl
 
 instance : comm_ring ℤ√d :=
 by refine_struct
@@ -108,7 +93,7 @@ by refine_struct
   one            := 1,
   npow           := @npow_rec (ℤ√d) ⟨1⟩ ⟨(*)⟩,
   nsmul          := @nsmul_rec (ℤ√d) ⟨0⟩ ⟨(+)⟩,
-  zsmul          := @zsmul_rec (ℤ√d) ⟨0⟩ ⟨(+)⟩ ⟨zsqrtd.neg⟩ };
+  zsmul          := @zsmul_rec (ℤ√d) ⟨0⟩ ⟨(+)⟩ ⟨has_neg.neg⟩ };
 intros; try { refl }; simp [ext, add_mul, mul_add, add_comm, add_left_comm, mul_comm, mul_left_comm]
 
 instance : add_comm_monoid ℤ√d    := by apply_instance
@@ -125,12 +110,9 @@ 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
+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
 
 /-- `conj` as an `add_monoid_hom`. -/
 def conj_hom : ℤ√d →+ ℤ√d :=
@@ -145,8 +127,7 @@ conj_hom.map_zero
 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_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
@@ -366,6 +347,7 @@ cast nonnegg_comm (nonnegg_cases_right h)
 
 section norm
 
+/-- The norm of an element of `ℤ[√d]`. -/
 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
 
@@ -458,21 +440,16 @@ parameter {d : ℕ}
 /-- Nonnegativity of an element of `ℤ√d`. -/
 def nonneg : ℤ√d → Prop | ⟨a, b⟩ := nonnegg d 1 a b
 
-protected def le (a b : ℤ√d) : Prop := nonneg (b - a)
-
-instance : has_le ℤ√d := ⟨zsqrtd.le⟩
-
-protected def lt (a b : ℤ√d) : Prop := ¬(b ≤ a)
-
-instance : has_lt ℤ√d := ⟨zsqrtd.lt⟩
+instance : has_le ℤ√d := ⟨λ a b, nonneg (b - a)⟩
+instance : has_lt ℤ√d := ⟨λ a b, ¬ b ≤ a⟩
 
 instance decidable_nonnegg (c d a b) : decidable (nonnegg c d a b) :=
 by cases a; cases b; repeat {rw int.of_nat_eq_coe}; unfold nonnegg sq_le; apply_instance
 
 instance decidable_nonneg : Π (a : ℤ√d), decidable (nonneg a)
 | ⟨a, b⟩ := zsqrtd.decidable_nonnegg _ _ _ _
 
-instance decidable_le (a b : ℤ√d) : decidable (a ≤ b) := decidable_nonneg _
+instance decidable_le : @decidable_rel (ℤ√d) (≤) := λ _ _, decidable_nonneg _
 
 theorem nonneg_cases : Π {a : ℤ√d}, nonneg a → ∃ x y : ℕ, a = ⟨x, y⟩ ∨ a = ⟨x, -y⟩ ∨ a = ⟨-x, y⟩
 | ⟨(x : ℕ), (y : ℕ)⟩ h := ⟨x, y, or.inl rfl⟩
@@ -498,10 +475,10 @@ have nonneg ⟨int.sub_nat_nat x z, int.sub_nat_nat w y⟩, from int.sub_nat_nat
 show nonneg ⟨_, _⟩, by rw [neg_add_eq_sub];
   rwa [int.sub_nat_nat_eq_coe,int.sub_nat_nat_eq_coe] at this
 
-theorem nonneg_add {a b : ℤ√d} (ha : nonneg a) (hb : nonneg b) : nonneg (a + b) :=
+lemma nonneg.add {a b : ℤ√d} (ha : nonneg a) (hb : nonneg b) : nonneg (a + b) :=
 begin
   rcases nonneg_cases ha with ⟨x, y, rfl|rfl|rfl⟩;
-  rcases nonneg_cases hb with ⟨z, w, rfl|rfl|rfl⟩; dsimp [add, nonneg] at ha hb ⊢,
+  rcases nonneg_cases hb with ⟨z, w, rfl|rfl|rfl⟩,
   { trivial },
   { refine nonnegg_cases_right (λi h, sq_le_of_le _ _ (nonnegg_pos_neg.1 hb)),
     { exact int.coe_nat_le.1 (le_of_neg_le_neg (@int.le.intro _ _ y (by simp [add_comm, *]))) },
@@ -518,32 +495,45 @@ begin
   { refine nonnegg_cases_left (λi h, sq_le_of_le _ _ (nonnegg_neg_pos.1 ha)),
     { exact int.coe_nat_le.1 (le_of_neg_le_neg (int.le.intro h)) },
     { apply nat.le_add_right } },
-  { rw [add_comm, add_comm ↑y], exact nonneg_add_lem hb ha },
+  { dsimp, rw [add_comm, add_comm ↑y], exact nonneg_add_lem hb ha },
   { simpa [add_comm] using
       nonnegg_neg_pos.2 (sq_le_add (nonnegg_neg_pos.1 ha) (nonnegg_neg_pos.1 hb)) },
 end
 
-theorem le_refl (a : ℤ√d) : a ≤ a := show nonneg (a - a), by simp
-
-protected theorem le_trans {a b c : ℤ√d} (ab : a ≤ b) (bc : b ≤ c) : a ≤ c :=
-have nonneg (b - a + (c - b)), from nonneg_add ab bc,
-by simpa [sub_add_sub_cancel']
-
 theorem nonneg_iff_zero_le {a : ℤ√d} : nonneg a ↔ 0 ≤ a := show _ ↔ nonneg _, by simp
 
 theorem le_of_le_le {x y z w : ℤ} (xz : x ≤ z) (yw : y ≤ w) : (⟨x, y⟩ : ℤ√d) ≤ ⟨z, w⟩ :=
 show nonneg ⟨z - x, w - y⟩, from
 match z - x, w - y, int.le.dest_sub xz, int.le.dest_sub yw with ._, ._, ⟨a, rfl⟩, ⟨b, rfl⟩ :=
   trivial end
 
+protected theorem nonneg_total : Π (a : ℤ√d), nonneg a ∨ nonneg (-a)
+| ⟨(x : ℕ), (y : ℕ)⟩ := or.inl trivial
+| ⟨-[1+ x], -[1+ y]⟩ := or.inr trivial
+| ⟨0,       -[1+ y]⟩ := or.inr trivial
+| ⟨-[1+ x], 0⟩       := or.inr trivial
+| ⟨(x+1:ℕ), -[1+ y]⟩ := nat.le_total
+| ⟨-[1+ x], (y+1:ℕ)⟩ := nat.le_total
+
+protected theorem le_total (a b : ℤ√d) : a ≤ b ∨ b ≤ a :=
+let t := nonneg_total (b - a) in by rw [show -(b-a) = a-b, from neg_sub b a] at t; exact t
+
+instance : preorder ℤ√d :=
+{ le               := (≤),
+  le_refl          := λ a, show nonneg (a - a), by simp only [sub_self],
+  le_trans         := λ a b c hab hbc, by simpa [sub_add_sub_cancel'] using hab.add hbc,
+  lt               := (<),
+  lt_iff_le_not_le := λ a b,
+    (and_iff_right_of_imp (zsqrtd.le_total _ _).resolve_left).symm }
+
 theorem le_arch (a : ℤ√d) : ∃n : ℕ, a ≤ n :=
 let ⟨x, y, (h : a ≤ ⟨x, y⟩)⟩ := show ∃x y : ℕ, nonneg (⟨x, y⟩ + -a), from match -a with
 | ⟨int.of_nat x, int.of_nat y⟩ := ⟨0, 0, trivial⟩
 | ⟨int.of_nat x, -[1+ y]⟩      := ⟨0, y+1, by simp [int.neg_succ_of_nat_coe, add_assoc]⟩
 | ⟨-[1+ x],      int.of_nat y⟩ := ⟨x+1, 0, by simp [int.neg_succ_of_nat_coe, add_assoc]⟩
 | ⟨-[1+ x],      -[1+ y]⟩      := ⟨x+1, y+1, by simp [int.neg_succ_of_nat_coe, add_assoc]⟩
 end in begin
-  refine ⟨x + d*y, zsqrtd.le_trans h _⟩,
+  refine ⟨x + d*y, h.trans _⟩,
   rw [← int.cast_coe_nat, ← of_int_eq_coe],
   change nonneg ⟨(↑x + d*y) - ↑x, 0-↑y⟩,
   cases y with y,
@@ -555,25 +545,6 @@ end in begin
   exact h (y+1)
 end
 
-protected theorem nonneg_total : Π (a : ℤ√d), nonneg a ∨ nonneg (-a)
-| ⟨(x : ℕ), (y : ℕ)⟩ := or.inl trivial
-| ⟨-[1+ x], -[1+ y]⟩ := or.inr trivial
-| ⟨0,       -[1+ y]⟩ := or.inr trivial
-| ⟨-[1+ x], 0⟩       := or.inr trivial
-| ⟨(x+1:ℕ), -[1+ y]⟩ := nat.le_total
-| ⟨-[1+ x], (y+1:ℕ)⟩ := nat.le_total
-
-protected theorem le_total (a b : ℤ√d) : a ≤ b ∨ b ≤ a :=
-let t := nonneg_total (b - a) in by rw [show -(b-a) = a-b, from neg_sub b a] at t; exact t
-
-instance : preorder ℤ√d :=
-{ le               := zsqrtd.le,
-  le_refl          := zsqrtd.le_refl,
-  le_trans         := @zsqrtd.le_trans,
-  lt               := zsqrtd.lt,
-  lt_iff_le_not_le := λ a b,
-    (and_iff_right_of_imp (zsqrtd.le_total _ _).resolve_left).symm }
-
 protected theorem add_le_add_left (a b : ℤ√d) (ab : a ≤ b) (c : ℤ√d) : c + a ≤ c + b :=
 show nonneg _, by rw add_sub_add_left_eq_sub; exact ab
 
@@ -606,7 +577,7 @@ end
 theorem nonneg_mul_lem {x y : ℕ} {a : ℤ√d} (ha : nonneg a) : nonneg (⟨x, y⟩ * a) :=
 have (⟨x, y⟩ * a : ℤ√d) = x * a + sqrtd * (y * a), by rw [decompose, right_distrib, mul_assoc];
   refl,
-by rw this; exact nonneg_add (nonneg_smul ha) (nonneg_muld $ nonneg_smul ha)
+by rw this; exact (nonneg_smul ha).add (nonneg_muld $ nonneg_smul ha)
 
 theorem nonneg_mul {a b : ℤ√d} (ha : nonneg a) (hb : nonneg b) : nonneg (a * b) :=
 match a, b, nonneg_cases ha, nonneg_cases hb, ha, hb with

src/number_theory/zsqrtd/gaussian_int.lean

@@ -37,6 +37,7 @@ and definitions about `zsqrtd` can easily be used.
 
 open zsqrtd complex
 
+/-- The Gaussian integers, defined as `ℤ√(-1)`. -/
 @[reducible] def gaussian_int : Type := zsqrtd (-1)
 
 local notation `ℤ[i]` := gaussian_int
@@ -106,12 +107,9 @@ lemma nat_abs_norm_eq (x : ℤ[i]) : x.norm.nat_abs =
   x.re.nat_abs * x.re.nat_abs + x.im.nat_abs * x.im.nat_abs :=
 int.coe_nat_inj $ begin simp, simp [norm] end
 
-protected def div (x y : ℤ[i]) : ℤ[i] :=
-let n := (rat.of_int (norm y))⁻¹ in let c := y.conj in
-⟨round (rat.of_int (x * c).re * n : ℚ),
- round (rat.of_int (x * c).im * n : ℚ)⟩
-
-instance : has_div ℤ[i] := ⟨gaussian_int.div⟩
+instance : has_div ℤ[i] :=
+⟨λ x y, let n := (rat.of_int (norm y))⁻¹, c := y.conj in
+  ⟨round (rat.of_int (x * c).re * n : ℚ), round (rat.of_int (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 : ℚ)⟩ :=
@@ -149,9 +147,7 @@ calc ((x / y : ℂ) - ((x / y : ℤ[i]) : ℂ)).norm_sq =
       simpa using abs_sub_round (x / y : ℂ).im)
   ... < 1 : by simp [norm_sq]; norm_num
 
-protected def mod (x y : ℤ[i]) : ℤ[i] := x - y * (x / y)
-
-instance : has_mod ℤ[i] := ⟨gaussian_int.mod⟩
+instance : has_mod ℤ[i] := ⟨λ x y, x - y * (x / y)⟩
 
 lemma mod_def (x y : ℤ[i]) : x % y = x - y * (x / y) := rfl