chore(data/{complex,is_R_or_C}/basic): fix name of eq_conj_iff_* le…

…mmas (#18922)

These were all about `conj x = x` not `x = conj x`.

src/analysis/complex/upper_half_plane/metric.lean

@@ -111,7 +111,7 @@ begin
     div_mul_eq_div_div _ _ (dist _ _), le_div_iff, div_mul_eq_mul_div],
   { exact div_le_div_of_le (mul_nonneg zero_le_two (sqrt_nonneg _))
       (euclidean_geometry.mul_dist_le_mul_dist_add_mul_dist (a : ℂ) b c (conj ↑b)) },
-  { rw [dist_comm, dist_pos, ne.def, complex.eq_conj_iff_im],
+  { rw [dist_comm, dist_pos, ne.def, complex.conj_eq_iff_im],
     exact b.im_ne_zero }
 end
 

src/analysis/inner_product_space/positive.lean

@@ -119,7 +119,7 @@ lemma is_positive_iff_complex (T : E' →L[ℂ] E') :
   is_positive T ↔ ∀ x, (re ⟪T x, x⟫_ℂ : ℂ) = ⟪T x, x⟫_ℂ ∧ 0 ≤ re ⟪T x, x⟫_ℂ :=
 begin
   simp_rw [is_positive, forall_and_distrib, is_self_adjoint_iff_is_symmetric,
-    linear_map.is_symmetric_iff_inner_map_self_real, eq_conj_iff_re],
+    linear_map.is_symmetric_iff_inner_map_self_real, conj_eq_iff_re],
   refl
 end
 

src/analysis/inner_product_space/spectrum.lean

@@ -205,7 +205,7 @@ begin
     have H₂ : v ≠ 0 := by simpa using (hT.eigenvector_basis hn).to_basis.ne_zero i,
     exact ⟨H₁, H₂⟩ },
   have re_μ : ↑(is_R_or_C.re μ) = μ,
-  { rw ← is_R_or_C.eq_conj_iff_re,
+  { rw ← is_R_or_C.conj_eq_iff_re,
     exact hT.conj_eigenvalue_eq_self (has_eigenvalue_of_has_eigenvector key) },
   simpa [re_μ] using key,
 end

src/analysis/inner_product_space/symmetric.lean

@@ -109,7 +109,7 @@ end
 begin
   rsuffices ⟨r, hr⟩ : ∃ r : ℝ, ⟪T x, x⟫ = r,
   { simp [hr, T.re_apply_inner_self_apply] },
-  rw ← eq_conj_iff_real,
+  rw ← conj_eq_iff_real,
   exact hT.conj_inner_sym x x
 end
 
@@ -165,7 +165,7 @@ begin
   { simp_rw [h, zero_mul, sub_zero, add_zero, map_add, map_sub, inner_add_left,
       inner_add_right, inner_sub_left, inner_sub_right, hT x, ← inner_conj_symm x (T y)],
     suffices : (re ⟪T y, x⟫ : 𝕜) = ⟪T y, x⟫,
-    { rw eq_conj_iff_re.mpr this,
+    { rw conj_eq_iff_re.mpr this,
       ring_nf, },
     { rw ← re_add_im ⟪T y, x⟫,
       simp_rw [h, mul_zero, add_zero],

src/analysis/special_functions/gamma.lean

@@ -612,7 +612,7 @@ lemma Gamma_one : Gamma 1 = 1 :=
 by rw [Gamma, complex.of_real_one, complex.Gamma_one, complex.one_re]
 
 lemma _root_.complex.Gamma_of_real (s : ℝ) : complex.Gamma (s : ℂ) = Gamma s :=
-by rw [Gamma, eq_comm, ←complex.eq_conj_iff_re, ←complex.Gamma_conj, complex.conj_of_real]
+by rw [Gamma, eq_comm, ←complex.conj_eq_iff_re, ←complex.Gamma_conj, complex.conj_of_real]
 
 theorem Gamma_nat_eq_factorial (n : ℕ) : Gamma (n + 1) = n! :=
 by rw [Gamma, complex.of_real_add, complex.of_real_nat_cast, complex.of_real_one,

src/data/complex/basic.lean

@@ -257,14 +257,14 @@ lemma conj_bit1 (z : ℂ) : conj (bit1 z) = bit1 (conj z) := ext_iff.2 $ by simp
 
 @[simp] lemma conj_neg_I : conj (-I) = I := ext_iff.2 $ by simp
 
-lemma eq_conj_iff_real {z : ℂ} : conj z = z ↔ ∃ r : ℝ, z = r :=
+lemma conj_eq_iff_real {z : ℂ} : conj z = z ↔ ∃ r : ℝ, z = r :=
 ⟨λ h, ⟨z.re, ext rfl $ eq_zero_of_neg_eq (congr_arg im h)⟩,
  λ ⟨h, e⟩, by rw [e, conj_of_real]⟩
 
-lemma eq_conj_iff_re {z : ℂ} : conj z = z ↔ (z.re : ℂ) = z :=
-eq_conj_iff_real.trans ⟨by rintro ⟨r, rfl⟩; simp, λ h, ⟨_, h.symm⟩⟩
+lemma conj_eq_iff_re {z : ℂ} : conj z = z ↔ (z.re : ℂ) = z :=
+conj_eq_iff_real.trans ⟨by rintro ⟨r, rfl⟩; simp, λ h, ⟨_, h.symm⟩⟩
 
-lemma eq_conj_iff_im {z : ℂ} : conj z = z ↔ z.im = 0 :=
+lemma conj_eq_iff_im {z : ℂ} : conj z = z ↔ z.im = 0 :=
 ⟨λ h, add_self_eq_zero.mp (neg_eq_iff_add_eq_zero.mp (congr_arg im h)),
   λ h, ext rfl (neg_eq_iff_add_eq_zero.mpr (add_self_eq_zero.mpr h))⟩
 

src/data/complex/exponential.lean

@@ -474,7 +474,7 @@ begin
 end
 
 @[simp] lemma of_real_exp_of_real_re (x : ℝ) : ((exp x).re : ℂ) = exp x :=
-eq_conj_iff_re.1 $ by rw [← exp_conj, conj_of_real]
+conj_eq_iff_re.1 $ by rw [← exp_conj, conj_of_real]
 
 @[simp, norm_cast] lemma of_real_exp (x : ℝ) : (real.exp x : ℂ) = exp x :=
 of_real_exp_of_real_re _
@@ -537,7 +537,7 @@ by rw [sinh, ← ring_hom.map_neg, exp_conj, exp_conj, ← ring_hom.map_sub, sin
   map_div₀, conj_bit0, ring_hom.map_one]
 
 @[simp] lemma of_real_sinh_of_real_re (x : ℝ) : ((sinh x).re : ℂ) = sinh x :=
-eq_conj_iff_re.1 $ by rw [← sinh_conj, conj_of_real]
+conj_eq_iff_re.1 $ by rw [← sinh_conj, conj_of_real]
 
 @[simp, norm_cast] lemma of_real_sinh (x : ℝ) : (real.sinh x : ℂ) = sinh x :=
 of_real_sinh_of_real_re _
@@ -554,7 +554,7 @@ begin
 end
 
 lemma of_real_cosh_of_real_re (x : ℝ) : ((cosh x).re : ℂ) = cosh x :=
-eq_conj_iff_re.1 $ by rw [← cosh_conj, conj_of_real]
+conj_eq_iff_re.1 $ by rw [← cosh_conj, conj_of_real]
 
 @[simp, norm_cast] lemma of_real_cosh (x : ℝ) : (real.cosh x : ℂ) = cosh x :=
 of_real_cosh_of_real_re _
@@ -574,7 +574,7 @@ lemma tanh_conj : tanh (conj x) = conj (tanh x) :=
 by rw [tanh, sinh_conj, cosh_conj, ← map_div₀, tanh]
 
 @[simp] lemma of_real_tanh_of_real_re (x : ℝ) : ((tanh x).re : ℂ) = tanh x :=
-eq_conj_iff_re.1 $ by rw [← tanh_conj, conj_of_real]
+conj_eq_iff_re.1 $ by rw [← tanh_conj, conj_of_real]
 
 @[simp, norm_cast] lemma of_real_tanh (x : ℝ) : (real.tanh x : ℂ) = tanh x :=
 of_real_tanh_of_real_re _
@@ -757,7 +757,7 @@ by rw [← mul_left_inj' I_ne_zero, ← sinh_mul_I,
        mul_neg, sinh_neg, sinh_mul_I, mul_neg]
 
 @[simp] lemma of_real_sin_of_real_re (x : ℝ) : ((sin x).re : ℂ) = sin x :=
-eq_conj_iff_re.1 $ by rw [← sin_conj, conj_of_real]
+conj_eq_iff_re.1 $ by rw [← sin_conj, conj_of_real]
 
 @[simp, norm_cast] lemma of_real_sin (x : ℝ) : (real.sin x : ℂ) = sin x :=
 of_real_sin_of_real_re _
@@ -772,7 +772,7 @@ by rw [← cosh_mul_I, ← conj_neg_I, ← ring_hom.map_mul, ← cosh_mul_I,
        cosh_conj, mul_neg, cosh_neg]
 
 @[simp] lemma of_real_cos_of_real_re (x : ℝ) : ((cos x).re : ℂ) = cos x :=
-eq_conj_iff_re.1 $ by rw [← cos_conj, conj_of_real]
+conj_eq_iff_re.1 $ by rw [← cos_conj, conj_of_real]
 
 @[simp, norm_cast] lemma of_real_cos (x : ℝ) : (real.cos x : ℂ) = cos x :=
 of_real_cos_of_real_re _
@@ -795,7 +795,7 @@ lemma tan_conj : tan (conj x) = conj (tan x) :=
 by rw [tan, sin_conj, cos_conj, ← map_div₀, tan]
 
 @[simp] lemma of_real_tan_of_real_re (x : ℝ) : ((tan x).re : ℂ) = tan x :=
-eq_conj_iff_re.1 $ by rw [← tan_conj, conj_of_real]
+conj_eq_iff_re.1 $ by rw [← tan_conj, conj_of_real]
 
 @[simp, norm_cast] lemma of_real_tan (x : ℝ) : (real.tan x : ℂ) = tan x :=
 of_real_tan_of_real_re _

src/data/is_R_or_C/basic.lean

@@ -224,7 +224,7 @@ begin
   simp only [one_mul, algebra.smul_mul_assoc],
 end
 
-lemma eq_conj_iff_real {z : K} : conj z = z ↔ ∃ r : ℝ, z = (r : K) :=
+lemma conj_eq_iff_real {z : K} : conj z = z ↔ ∃ r : ℝ, z = (r : K) :=
 begin
   split,
   { intro h,
@@ -249,8 +249,8 @@ abbreviation conj_to_ring_equiv : K ≃+* Kᵐᵒᵖ := star_ring_equiv
 
 variables {K}
 
-lemma eq_conj_iff_re {z : K} : conj z = z ↔ ((re z) : K) = z :=
-eq_conj_iff_real.trans ⟨by rintro ⟨r, rfl⟩; simp, λ h, ⟨_, h.symm⟩⟩
+lemma conj_eq_iff_re {z : K} : conj z = z ↔ ((re z) : K) = z :=
+conj_eq_iff_real.trans ⟨by rintro ⟨r, rfl⟩; simp, λ h, ⟨_, h.symm⟩⟩
 
 /-- The norm squared function. -/
 def norm_sq : K →*₀ ℝ :=

src/field_theory/polynomial_galois_group.lean

@@ -374,7 +374,7 @@ begin
     (restrict p ℂ (complex.conj_ae.restrict_scalars ℚ)) w = w ↔ w.val.im = 0,
   { intro w,
     rw [subtype.ext_iff, gal_action_hom_restrict],
-    exact complex.eq_conj_iff_im },
+    exact complex.conj_eq_iff_im },
   have hc : ∀ z : ℂ, z ∈ c ↔ aeval z p = 0 ∧ z.im ≠ 0,
   { intro z,
     simp_rw [finset.mem_image, exists_prop],

src/linear_algebra/matrix/hermitian.lean

@@ -227,7 +227,7 @@ variables [is_R_or_C α] [is_R_or_C β]
 /-- The diagonal elements of a complex hermitian matrix are real. -/
 lemma is_hermitian.coe_re_apply_self {A : matrix n n α} (h : A.is_hermitian) (i : n) :
   (re (A i i) : α) = A i i :=
-by rw [←eq_conj_iff_re, ←star_def, ←conj_transpose_apply, h.eq]
+by rw [←conj_eq_iff_re, ←star_def, ←conj_transpose_apply, h.eq]
 
 /-- The diagonal elements of a complex hermitian matrix are real. -/
 lemma is_hermitian.coe_re_diag {A : matrix n n α} (h : A.is_hermitian) :

src/number_theory/number_field/embeddings.lean

@@ -172,7 +172,7 @@ lemma is_real_iff {φ : K →+* ℂ} : is_real φ ↔ conjugate φ = φ := is_se
 def is_real.embedding {φ : K →+* ℂ} (hφ : is_real φ) : K →+* ℝ :=
 { to_fun := λ x, (φ x).re,
   map_one' := by simp only [map_one, one_re],
-  map_mul' := by simp only [complex.eq_conj_iff_im.mp (ring_hom.congr_fun hφ _), map_mul, mul_re,
+  map_mul' := by simp only [complex.conj_eq_iff_im.mp (ring_hom.congr_fun hφ _), map_mul, mul_re,
   mul_zero, tsub_zero, eq_self_iff_true, forall_const],
   map_zero' := by simp only [map_zero, zero_re],
   map_add' := by simp only [map_add, add_re, eq_self_iff_true, forall_const], }
@@ -182,7 +182,7 @@ lemma is_real.coe_embedding_apply {φ : K →+* ℂ} (hφ : is_real φ) (x : K)
   (hφ.embedding x : ℂ) = φ x :=
 begin
   ext, { refl, },
-  { rw [of_real_im, eq_comm, ← complex.eq_conj_iff_im],
+  { rw [of_real_im, eq_comm, ← complex.conj_eq_iff_im],
     rw is_real at hφ,
     exact ring_hom.congr_fun hφ x, },
 end