changing names

leanprover-community · Mar 2, 2019 · 5cbd7fa · 5cbd7fa
1 parent a9dfaba
commit 5cbd7fa
Show file tree

Hide file tree

Showing 2 changed files with 8 additions and 8 deletions.
diff --git a/src/data/gaussian_int.lean b/src/data/gaussian_int.lean
@@ -37,10 +37,10 @@ by refine_struct {..}; intros; apply complex.ext; simp [to_complex]
 
 instance : is_ring_hom (coe : ℤ[i] → ℂ) := to_complex.is_ring_hom
 
-@[simp] lemma int_cast_re (x : ℤ[i]) : ((x.re : ℤ) : ℝ) = (x : ℂ).re := by simp [to_complex_def]
-@[simp] lemma int_cast_im (x : ℤ[i]) : ((x.im : ℤ) : ℝ) = (x : ℂ).im := by simp [to_complex_def]
-@[simp] lemma to_complex_re' (x y : ℤ) : ((⟨x, y⟩ : ℤ[i]) : ℂ).re = x := by simp [to_complex_def]
-@[simp] lemma to_complex_im' (x y : ℤ) : ((⟨x, y⟩ : ℤ[i]) : ℂ).im = y := by simp [to_complex_def]
+@[simp] lemma to_real_re (x : ℤ[i]) : ((x.re : ℤ) : ℝ) = (x : ℂ).re := by simp [to_complex_def]
+@[simp] lemma to_real_im (x : ℤ[i]) : ((x.im : ℤ) : ℝ) = (x : ℂ).im := by simp [to_complex_def]
+@[simp] lemma to_complex_re (x y : ℤ) : ((⟨x, y⟩ : ℤ[i]) : ℂ).re = x := by simp [to_complex_def]
+@[simp] lemma to_complex_im (x y : ℤ) : ((⟨x, y⟩ : ℤ[i]) : ℂ).im = y := by simp [to_complex_def]
 @[simp] lemma to_complex_add (x y : ℤ[i]) : ((x + y : ℤ[i]) : ℂ) = x + y := is_ring_hom.map_add coe
 @[simp] lemma to_complex_mul (x y : ℤ[i]) : ((x * y : ℤ[i]) : ℂ) = x * y := is_ring_hom.map_mul coe
 @[simp] lemma to_complex_one : ((1 : ℤ[i]) : ℂ) = 1 := is_ring_hom.map_one coe

diff --git a/src/data/zmod/quadratic_reciprocity.lean b/src/data/zmod/quadratic_reciprocity.lean
@@ -41,7 +41,7 @@ lemma euler_criterion {a : zmodp p hp} (ha : a ≠ 0) :
 λ h, let ⟨y, hy⟩ := (euler_criterion_units hp).2 (show units.mk0 _ ha ^ (p / 2) = 1, by simpa [units.ext_iff]) in
   ⟨y, by simpa [units.ext_iff] using hy⟩⟩
 
-lemma neg_one_is_square_iff_mod_four_ne_three :
+lemma exists_pow_two_eq_neg_one_iff_mod_four_ne_three :
   (∃ y : zmodp p hp, y ^ 2 = -1) ↔ p % 4 ≠ 3 :=
 have (-1 : zmodp p hp) ≠ 0, from mt neg_eq_zero.1 one_ne_zero,
 hp.eq_two_or_odd.elim (λ hp, by subst hp; exact dec_trivial)
@@ -534,7 +534,7 @@ begin
   cc
 end
 
-lemma is_square_iff_is_square_of_mod_four_eq_one (hp1 : p % 4 = 1) (hq1 : q % 2 = 1) :
+lemma exists_pow_two_eq_prime_iff_of_mod_four_eq_one (hp1 : p % 4 = 1) (hq1 : q % 2 = 1) :
   (∃ a : zmodp p hp, a ^ 2 = q) ↔ ∃ b : zmodp q hq, b ^ 2 = p :=
 if hpq : p = q then by subst hpq else
 have h1 : ((p / 2) * (q / 2)) % 2 = 0,
@@ -549,8 +549,8 @@ begin
   split_ifs at this; simp *; contradiction
 end
 
-lemma is_square_iff_is_not_square_of_mod_four_eq_three (hp3 : p % 4 = 3) (hq3 : q % 4 = 3)
-  (hpq : p ≠ q) : (∃ a : zmodp p hp, a ^ 2 = q) ↔ ¬∃ b : zmodp q hq, b ^ 2 = p :=
+lemma exists_pow_two_eq_prime_iff_of_mod_four_eq_three (hp3 : p % 4 = 3)
+  (hq3 : q % 4 = 3) (hpq : p ≠ q) : (∃ a : zmodp p hp, a ^ 2 = q) ↔ ¬∃ b : zmodp q hq, b ^ 2 = p :=
 have h1 : ((p / 2) * (q / 2)) % 2 = 1,
   from nat.odd_mul_odd
     (by rw [← mod_mul_right_div_self, show 2 * 2 = 4, from rfl, hp3]; refl)