feat(algebra/star/basic): change star_ring_aut (notably, complex co…

…njugation) from `ring_equiv` to `ring_hom` and make type argument explicit (#11418)

Change the underlying object notated by `conj` from
```lean
def star_ring_aut [comm_semiring R] [star_ring R] : ring_aut R :=
```
to
```lean
def star_ring_end [comm_semiring R] [star_ring R] : R →+* R :=
```
and also make the `R` argument explicit.  These two changes allow the notation for conjugate-linear maps, `E →ₗ⋆[R] F` and variants, to pretty-print, see
https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Pretty.20printer.20omits.20notation

This is a partial reversion of #9640, in which complex conjugation was upgraded from `ring_hom` to `ring_equiv`.

src/algebra/module/linear_map.lean

@@ -94,7 +94,7 @@ add_decl_doc linear_map.to_add_hom
 
 notation M ` →ₛₗ[`:25 σ:25 `] `:0 M₂:0 := linear_map σ M M₂
 notation M ` →ₗ[`:25 R:25 `] `:0 M₂:0 := linear_map (ring_hom.id R) M M₂
-notation M ` →ₗ⋆[`:25 R:25 `] `:0 M₂:0 := linear_map (@star_ring_aut R _ _ : R →+* R) M M₂
+notation M ` →ₗ⋆[`:25 R:25 `] `:0 M₂:0 := linear_map (star_ring_end R) M M₂
 
 namespace linear_map
 

src/algebra/star/basic.lean

@@ -231,29 +231,40 @@ instance star_ring.to_star_add_monoid [semiring R] [star_ring R] : star_add_mono
 def star_ring_equiv [semiring R] [star_ring R] : R ≃+* Rᵐᵒᵖ :=
 { to_fun := λ x, mul_opposite.op (star x),
   ..star_add_equiv.trans (mul_opposite.op_add_equiv : R ≃+ Rᵐᵒᵖ),
-  ..star_mul_equiv}
+  ..star_mul_equiv }
 
-/-- `star` as a `ring_aut` for commutative `R`. This is used to denote complex
-conjugation, and is available under the notation `conj` in the locale `complex_conjugate` -/
+/-- `star` as a ring automorphism, for commutative `R`. -/
+@[simps apply]
 def star_ring_aut [comm_semiring R] [star_ring R] : ring_aut R :=
 { to_fun := star,
   ..star_add_equiv,
   ..star_mul_aut }
 
-localized "notation `conj` := star_ring_aut" in complex_conjugate
+variables (R)
+/-- `star` as a ring endomorphism, for commutative `R`. This is used to denote complex
+conjugation, and is available under the notation `conj` in the locale `complex_conjugate`.
+
+Note that this is the preferred form (over `star_ring_aut`, available under the same hypotheses)
+because the notation `E →ₗ⋆[R] F` for an `R`-conjugate-linear map (short for
+`E →ₛₗ[star_ring_end R] F`) does not pretty-print if there is a coercion involved, as would be the
+case for `(↑star_ring_aut : R →* R)`. -/
+def star_ring_end [comm_semiring R] [star_ring R] : R →+* R := @star_ring_aut R _ _
+variables {R}
+
+localized "notation `conj` := star_ring_end _" in complex_conjugate
 
-/-- This is not a simp lemma, since we usually want simp to keep `star_ring_aut` bundled.
+/-- This is not a simp lemma, since we usually want simp to keep `star_ring_end` bundled.
  For example, for complex conjugation, we don't want simp to turn `conj x`
  into the bare function `star x` automatically since most lemmas are about `conj x`. -/
-lemma star_ring_aut_apply [comm_semiring R] [star_ring R] {x : R} :
-  star_ring_aut x = star x := rfl
+lemma star_ring_end_apply [comm_semiring R] [star_ring R] {x : R} :
+  star_ring_end R x = star x := rfl
 
-@[simp] lemma star_ring_aut_self_apply [comm_semiring R] [star_ring R] (x : R) :
-  star_ring_aut (star_ring_aut x) = x := star_star x
+@[simp] lemma star_ring_end_self_apply [comm_semiring R] [star_ring R] (x : R) :
+  star_ring_end R (star_ring_end R x) = x := star_star x
 
 -- A more convenient name for complex conjugation
-alias star_ring_aut_self_apply ← complex.conj_conj
-alias star_ring_aut_self_apply ← is_R_or_C.conj_conj
+alias star_ring_end_self_apply ← complex.conj_conj
+alias star_ring_end_self_apply ← is_R_or_C.conj_conj
 
 @[simp] lemma star_inv' [division_ring R] [star_ring R] (x : R) : star (x⁻¹) = (star x)⁻¹ :=
 op_injective $
@@ -266,7 +277,7 @@ op_injective $
 
 /-- When multiplication is commutative, `star` preserves division. -/
 @[simp] lemma star_div' [field R] [star_ring R] (x y : R) : star (x / y) = star x / star y :=
-(star_ring_aut : R ≃+* R).to_ring_hom.map_div _ _
+(star_ring_end R).map_div _ _
 
 @[simp] lemma star_bit0 [ring R] [star_ring R] (r : R) : star (bit0 r) = bit0 (star r) :=
 by simp [bit0]
@@ -340,8 +351,7 @@ namespace ring_hom_inv_pair
 /-- Instance needed to define star-linear maps over a commutative star ring
 (ex: conjugate-linear maps when R = ℂ).  -/
 instance [comm_semiring R] [star_ring R] :
-  ring_hom_inv_pair ((star_ring_aut : ring_aut R) : R →+* R)
-    ((star_ring_aut : ring_aut R) : R →+* R) :=
+  ring_hom_inv_pair (star_ring_end R) (star_ring_end R) :=
 ⟨ring_hom.ext star_star, ring_hom.ext star_star⟩
 
 end ring_hom_inv_pair

src/analysis/complex/circle.lean

@@ -65,7 +65,7 @@ instance : comm_group circle :=
     ← mul_self_abs] },
   .. circle.to_comm_monoid }
 
-lemma coe_inv_circle_eq_conj (z : circle) : ↑(z⁻¹) = (conj : ring_aut ℂ) z := rfl
+lemma coe_inv_circle_eq_conj (z : circle) : ↑(z⁻¹) = conj (z : ℂ) := rfl
 
 @[simp] lemma coe_inv_circle (z : circle) : ↑(z⁻¹) = (z : ℂ)⁻¹ :=
 begin

src/analysis/complex/isometry.lean

@@ -47,7 +47,7 @@ begin
   intro h,
   have h1 : rotation a 1 = conj 1 := linear_isometry_equiv.congr_fun h 1,
   have hI : rotation a I = conj I := linear_isometry_equiv.congr_fun h I,
-  rw [rotation_apply, ring_equiv.map_one, mul_one] at h1,
+  rw [rotation_apply, ring_hom.map_one, mul_one] at h1,
   rw [rotation_apply, conj_I, ← neg_one_mul, mul_left_inj' I_ne_zero, h1, eq_neg_self_iff] at hI,
   exact one_ne_zero hI,
 end
@@ -87,11 +87,11 @@ begin
   apply_fun λ x, x ^ 2 at this,
   simp only [norm_eq_abs, ←norm_sq_eq_abs] at this,
   rw [←of_real_inj, ←mul_conj, ←mul_conj] at this,
-  rw [ring_equiv.map_sub, ring_equiv.map_sub] at this,
+  rw [ring_hom.map_sub, ring_hom.map_sub] at this,
   simp only [sub_mul, mul_sub, one_mul, mul_one] at this,
   rw [mul_conj, norm_sq_eq_abs, ←norm_eq_abs, linear_isometry.norm_map] at this,
   rw [mul_conj, norm_sq_eq_abs, ←norm_eq_abs] at this,
-  simp only [sub_sub, sub_right_inj, mul_one, of_real_pow, ring_equiv.map_one, norm_eq_abs] at this,
+  simp only [sub_sub, sub_right_inj, mul_one, of_real_pow, ring_hom.map_one, norm_eq_abs] at this,
   simp only [add_sub, sub_left_inj] at this,
   rw [add_comm, ←this, add_comm],
 end

src/analysis/inner_product_space/basic.lean

@@ -152,7 +152,7 @@ local notation `norm_sqK` := @is_R_or_C.norm_sq 𝕜 _
 local notation `reK` := @is_R_or_C.re 𝕜 _
 local notation `absK` := @is_R_or_C.abs 𝕜 _
 local notation `ext_iff` := @is_R_or_C.ext_iff 𝕜 _
-local postfix `†`:90 := star_ring_aut
+local postfix `†`:90 := star_ring_end _
 
 /-- Inner product defined by the `inner_product_space.core` structure. -/
 def to_has_inner : has_inner 𝕜 F := { inner := c.inner }
@@ -177,7 +177,7 @@ lemma inner_add_left {x y z : F} : ⟪x + y, z⟫ = ⟪x, z⟫ + ⟪y, z⟫ :=
 c.add_left _ _ _
 
 lemma inner_add_right {x y z : F} : ⟪x, y + z⟫ = ⟪x, y⟫ + ⟪x, z⟫ :=
-by rw [←inner_conj_sym, inner_add_left, ring_equiv.map_add]; simp only [inner_conj_sym]
+by rw [←inner_conj_sym, inner_add_left, ring_hom.map_add]; simp only [inner_conj_sym]
 
 lemma inner_norm_sq_eq_inner_self (x : F) : (norm_sqF x : 𝕜) = ⟪x, x⟫ :=
 begin
@@ -195,13 +195,13 @@ lemma inner_smul_left {x y : F} {r : 𝕜} : ⟪r • x, y⟫ = r† * ⟪x, y
 c.smul_left _ _ _
 
 lemma inner_smul_right {x y : F} {r : 𝕜} : ⟪x, r • y⟫ = r * ⟪x, y⟫ :=
-by rw [←inner_conj_sym, inner_smul_left]; simp only [conj_conj, inner_conj_sym, ring_equiv.map_mul]
+by rw [←inner_conj_sym, inner_smul_left]; simp only [conj_conj, inner_conj_sym, ring_hom.map_mul]
 
 lemma inner_zero_left {x : F} : ⟪0, x⟫ = 0 :=
-by rw [←zero_smul 𝕜 (0 : F), inner_smul_left]; simp only [zero_mul, ring_equiv.map_zero]
+by rw [←zero_smul 𝕜 (0 : F), inner_smul_left]; simp only [zero_mul, ring_hom.map_zero]
 
 lemma inner_zero_right {x : F} : ⟪x, 0⟫ = 0 :=
-by rw [←inner_conj_sym, inner_zero_left]; simp only [ring_equiv.map_zero]
+by rw [←inner_conj_sym, inner_zero_left]; simp only [ring_hom.map_zero]
 
 lemma inner_self_eq_zero {x : F} : ⟪x, x⟫ = 0 ↔ x = 0 :=
 iff.intro (c.definite _) (by { rintro rfl, exact inner_zero_left })
@@ -216,7 +216,7 @@ lemma inner_neg_left {x y : F} : ⟪-x, y⟫ = -⟪x, y⟫ :=
 by { rw [← neg_one_smul 𝕜 x, inner_smul_left], simp }
 
 lemma inner_neg_right {x y : F} : ⟪x, -y⟫ = -⟪x, y⟫ :=
-by rw [←inner_conj_sym, inner_neg_left]; simp only [ring_equiv.map_neg, inner_conj_sym]
+by rw [←inner_conj_sym, inner_neg_left]; simp only [ring_hom.map_neg, inner_conj_sym]
 
 lemma inner_sub_left {x y z : F} : ⟪x - y, z⟫ = ⟪x, z⟫ - ⟪y, z⟫ :=
 by { simp [sub_eq_add_neg, inner_add_left, inner_neg_left] }
@@ -273,7 +273,7 @@ begin
       ... = re ⟪x, x⟫ - re (T† * ⟪y, x⟫) - re (T * ⟪x, y⟫) + re (T * T† * ⟪y, y⟫)
                   : by simp only [inner_smul_left, inner_smul_right, mul_assoc]
       ... = re ⟪x, x⟫ - re (⟪x, y⟫ / ⟪y, y⟫ * ⟪y, x⟫)
-                  : by field_simp [-mul_re, inner_conj_sym, hT, ring_equiv.map_div, h₁, h₃]
+                  : by field_simp [-mul_re, inner_conj_sym, hT, ring_hom.map_div, h₁, h₃]
       ... = re ⟪x, x⟫ - re (⟪x, y⟫ * ⟪y, x⟫ / ⟪y, y⟫)
                   : by rw [div_mul_eq_mul_div_comm, ←mul_div_assoc]
       ... = re ⟪x, x⟫ - re (⟪x, y⟫ * ⟪y, x⟫ / re ⟪y, y⟫)
@@ -386,7 +386,7 @@ local notation `⟪`x`, `y`⟫` := @inner 𝕜 _ _ x y
 local notation `IK` := @is_R_or_C.I 𝕜 _
 local notation `absR` := has_abs.abs
 local notation `absK` := @is_R_or_C.abs 𝕜 _
-local postfix `†`:90 := star_ring_aut
+local postfix `†`:90 := star_ring_end _
 
 export inner_product_space (norm_sq_eq_inner)
 
@@ -407,7 +407,7 @@ lemma inner_add_left {x y z : E} : ⟪x + y, z⟫ = ⟪x, z⟫ + ⟪y, z⟫ :=
 inner_product_space.add_left _ _ _
 
 lemma inner_add_right {x y z : E} : ⟪x, y + z⟫ = ⟪x, y⟫ + ⟪x, z⟫ :=
-by { rw [←inner_conj_sym, inner_add_left, ring_equiv.map_add], simp only [inner_conj_sym] }
+by { rw [←inner_conj_sym, inner_add_left, ring_hom.map_add], simp only [inner_conj_sym] }
 
 lemma inner_re_symm {x y : E} : re ⟪x, y⟫ = re ⟪y, x⟫ :=
 by rw [←inner_conj_sym, conj_re]
@@ -423,7 +423,7 @@ lemma inner_smul_real_left {x y : E} {r : ℝ} : ⟪(r : 𝕜) • x, y⟫ = r 
 by { rw [inner_smul_left, conj_of_real, algebra.smul_def], refl }
 
 lemma inner_smul_right {x y : E} {r : 𝕜} : ⟪x, r • y⟫ = r * ⟪x, y⟫ :=
-by rw [←inner_conj_sym, inner_smul_left, ring_equiv.map_mul, conj_conj, inner_conj_sym]
+by rw [←inner_conj_sym, inner_smul_left, ring_hom.map_mul, conj_conj, inner_conj_sym]
 lemma real_inner_smul_right {x y : F} {r : ℝ} : ⟪x, r • y⟫_ℝ = r * ⟪x, y⟫_ℝ := inner_smul_right
 
 lemma inner_smul_real_right {x y : E} {r : ℝ} : ⟪x, (r : 𝕜) • y⟫ = r • ⟪x, y⟫ :=
@@ -432,7 +432,7 @@ by { rw [inner_smul_right, algebra.smul_def], refl }
 /-- The inner product as a sesquilinear form. -/
 @[simps]
 def sesq_form_of_inner : E →ₗ[𝕜] E →ₗ⋆[𝕜] 𝕜 :=
-linear_map.mk₂'ₛₗ (ring_hom.id 𝕜) (star_ring_aut.to_ring_hom)
+linear_map.mk₂'ₛₗ (ring_hom.id 𝕜) (star_ring_end _)
   (λ x y, ⟪y, x⟫)
   (λ x y z, inner_add_right)
   (λ r x y, inner_smul_right)
@@ -480,13 +480,13 @@ lemma dfinsupp.inner_sum {ι : Type*} [dec : decidable_eq ι] {α : ι → Type*
 by simp [dfinsupp.sum, inner_sum] {contextual := tt}
 
 @[simp] lemma inner_zero_left {x : E} : ⟪0, x⟫ = 0 :=
-by rw [← zero_smul 𝕜 (0:E), inner_smul_left, ring_equiv.map_zero, zero_mul]
+by rw [← zero_smul 𝕜 (0:E), inner_smul_left, ring_hom.map_zero, zero_mul]
 
 lemma inner_re_zero_left {x : E} : re ⟪0, x⟫ = 0 :=
 by simp only [inner_zero_left, add_monoid_hom.map_zero]
 
 @[simp] lemma inner_zero_right {x : E} : ⟪x, 0⟫ = 0 :=
-by rw [←inner_conj_sym, inner_zero_left, ring_equiv.map_zero]
+by rw [←inner_conj_sym, inner_zero_left, ring_hom.map_zero]
 
 lemma inner_re_zero_right {x : E} : re ⟪x, 0⟫ = 0 :=
 by simp only [inner_zero_right, add_monoid_hom.map_zero]
@@ -553,7 +553,7 @@ by rw [←inner_conj_sym, abs_conj]
 by { rw [← neg_one_smul 𝕜 x, inner_smul_left], simp }
 
 @[simp] lemma inner_neg_right {x y : E} : ⟪x, -y⟫ = -⟪x, y⟫ :=
-by rw [←inner_conj_sym, inner_neg_left]; simp only [ring_equiv.map_neg, inner_conj_sym]
+by rw [←inner_conj_sym, inner_neg_left]; simp only [ring_hom.map_neg, inner_conj_sym]
 
 lemma inner_neg_neg {x y : E} : ⟪-x, -y⟫ = ⟪x, y⟫ := by simp
 
@@ -632,7 +632,7 @@ begin
       ... = re ⟪x, x⟫ - re (T† * ⟪y, x⟫) - re (T * ⟪x, y⟫) + re (T * T† * ⟪y, y⟫)
                   : by simp only [inner_smul_left, inner_smul_right, mul_assoc]
       ... = re ⟪x, x⟫ - re (⟪x, y⟫ / ⟪y, y⟫ * ⟪y, x⟫)
-                  : by field_simp [-mul_re, hT, ring_equiv.map_div, h₁, h₃, inner_conj_sym]
+                  : by field_simp [-mul_re, hT, ring_hom.map_div, h₁, h₃, inner_conj_sym]
       ... = re ⟪x, x⟫ - re (⟪x, y⟫ * ⟪y, x⟫ / ⟪y, y⟫)
                   : by rw [div_mul_eq_mul_div_comm, ←mul_div_assoc]
       ... = re ⟪x, x⟫ - re (⟪x, y⟫ * ⟪y, x⟫ / re ⟪y, y⟫)
@@ -1493,7 +1493,8 @@ end
 
 /-- The inner product as a continuous sesquilinear map, with the two arguments flipped. -/
 def innerSL_flip : E →L[𝕜] E →L⋆[𝕜] 𝕜 :=
-continuous_linear_map.flipₗᵢ' E E 𝕜 (ring_hom.id 𝕜) (↑star_ring_aut : 𝕜 →+* 𝕜) innerSL
+@continuous_linear_map.flipₗᵢ' 𝕜 𝕜 𝕜 E E 𝕜 _ _ _ _ _ _ _ _ _ (ring_hom.id 𝕜) (star_ring_end 𝕜) _ _
+  innerSL
 
 @[simp] lemma innerSL_flip_apply {x y : E} : innerSL_flip x y = ⟪y, x⟫ := rfl
 
@@ -1505,7 +1506,7 @@ variables  {E' : Type*} [inner_product_space 𝕜 E']
 as a continuous linear map. -/
 def to_sesq_form : (E →L[𝕜] E') →L[𝕜] E' →L⋆[𝕜] E →L[𝕜] 𝕜 :=
 ↑((continuous_linear_map.flipₗᵢ' E E' 𝕜
-  (↑(star_ring_aut : 𝕜 ≃+* 𝕜) : 𝕜 →+* 𝕜) (ring_hom.id 𝕜)).to_continuous_linear_equiv) ∘L
+  (star_ring_end 𝕜) (ring_hom.id 𝕜)).to_continuous_linear_equiv) ∘L
 (continuous_linear_map.compSL E E' (E' →L⋆[𝕜] 𝕜) (ring_hom.id 𝕜) (ring_hom.id 𝕜) innerSL_flip)
 
 @[simp] lemma to_sesq_form_apply_coe (f : E →L[𝕜] E') (x : E') :

src/analysis/inner_product_space/dual.lean

@@ -39,7 +39,7 @@ open is_R_or_C continuous_linear_map
 variables (𝕜 : Type*)
 variables (E : Type*) [is_R_or_C 𝕜] [inner_product_space 𝕜 E]
 local notation `⟪`x`, `y`⟫` := @inner 𝕜 E _ x y
-local postfix `†`:90 := star_ring_aut
+local postfix `†`:90 := star_ring_end _
 
 /--
 An element `x` of an inner product space `E` induces an element of the dual space `dual 𝕜 E`,
@@ -96,7 +96,7 @@ begin
       exact sub_eq_zero.mp (eq.symm h₃) },
     have h₄ := calc
       ⟪((ℓ z)† / ⟪z, z⟫) • z, x⟫ = (ℓ z) / ⟪z, z⟫ * ⟪z, x⟫
-            : by simp [inner_smul_left, ring_equiv.map_div, conj_conj]
+            : by simp [inner_smul_left, ring_hom.map_div, conj_conj]
                             ... = (ℓ z) * ⟪z, x⟫ / ⟪z, z⟫
             : by rw [←div_mul_eq_mul_div]
                             ... = (ℓ x) * ⟪z, z⟫ / ⟪z, z⟫

src/analysis/inner_product_space/pi_L2.lean

@@ -71,7 +71,7 @@ instance pi_Lp.inner_product_space {ι : Type*} [fintype ι] (f : ι → Type*)
   begin
     intros x y,
     unfold inner,
-    rw ring_equiv.map_sum,
+    rw ring_hom.map_sum,
     apply finset.sum_congr rfl,
     rintros z -,
     apply inner_conj_sym,

src/analysis/normed_space/linear_isometry.lean

@@ -48,7 +48,7 @@ structure linear_isometry (σ₁₂ : R →+* R₂) (E E₂ : Type*) [semi_norme
 
 notation E ` →ₛₗᵢ[`:25 σ₁₂:25 `] `:0 E₂:0 := linear_isometry σ₁₂ E E₂
 notation E ` →ₗᵢ[`:25 R:25 `] `:0 E₂:0 := linear_isometry (ring_hom.id R) E E₂
-notation E ` →ₗᵢ⋆[`:25 R:25 `] `:0 E₂:0 := linear_isometry (@star_ring_aut R _ _ : R →+* R) E E₂
+notation E ` →ₗᵢ⋆[`:25 R:25 `] `:0 E₂:0 := linear_isometry (star_ring_end R) E E₂
 
 namespace linear_isometry
 
@@ -245,7 +245,7 @@ structure linear_isometry_equiv (σ₁₂ : R →+* R₂) {σ₂₁ : R₂ →+*
 notation E ` ≃ₛₗᵢ[`:25 σ₁₂:25 `] `:0 E₂:0 := linear_isometry_equiv σ₁₂ E E₂
 notation E ` ≃ₗᵢ[`:25 R:25 `] `:0 E₂:0 := linear_isometry_equiv (ring_hom.id R) E E₂
 notation E ` ≃ₗᵢ⋆[`:25 R:25 `] `:0 E₂:0 :=
-  linear_isometry_equiv (@star_ring_aut R _ _ : R →+* R) E E₂
+  linear_isometry_equiv (star_ring_end R) E E₂
 
 namespace linear_isometry_equiv
 

src/analysis/normed_space/star.lean

@@ -95,8 +95,8 @@ lemma continuous_within_at.star {f : α → E} {s : set α} {x : α}
 
 end normed_star_monoid
 
-instance ring_hom_isometric.star_ring_aut [normed_comm_ring E] [star_ring E]
-   [normed_star_monoid E] : ring_hom_isometric ((star_ring_aut : ring_aut E) : E →+* E) :=
+instance ring_hom_isometric.star_ring_end [normed_comm_ring E] [star_ring E]
+   [normed_star_monoid E] : ring_hom_isometric (star_ring_end E) :=
 ⟨λ _, norm_star⟩
 
 namespace cstar_ring

src/data/complex/basic.lean

@@ -186,7 +186,7 @@ by rw [pow_bit1', I_mul_I]
 /-! ### Complex conjugation -/
 
 /-- This defines the complex conjugate as the `star` operation of the `star_ring ℂ`. It
-is recommended to use the ring automorphism version `star_ring_aut`, available under the
+is recommended to use the ring endomorphism version `star_ring_end`, available under the
 notation `conj` in the locale `complex_conjugate`. -/
 instance : star_ring ℂ :=
 { star := λ z, ⟨z.re, -z.im⟩,
@@ -301,7 +301,7 @@ ext_iff.2 $ by simp [two_mul, sub_eq_add_neg]
 lemma norm_sq_sub (z w : ℂ) : norm_sq (z - w) =
   norm_sq z + norm_sq w - 2 * (z * conj w).re :=
 by { rw [sub_eq_add_neg, norm_sq_add],
-     simp only [ring_equiv.map_neg, mul_neg_eq_neg_mul_symm, neg_re,
+     simp only [ring_hom.map_neg, mul_neg_eq_neg_mul_symm, neg_re,
                 tactic.ring.add_neg_eq_sub, norm_sq_neg] }
 
 /-! ### Inversion -/
@@ -657,7 +657,7 @@ by rw [lim_eq_lim_im_add_lim_re]; simp
 
 lemma is_cau_seq_conj (f : cau_seq ℂ abs) : is_cau_seq abs (λ n, conj (f n)) :=
 λ ε ε0, let ⟨i, hi⟩ := f.2 ε ε0 in
-⟨i, λ j hj, by rw [← ring_equiv.map_sub, abs_conj]; exact hi j hj⟩
+⟨i, λ j hj, by rw [← ring_hom.map_sub, abs_conj]; exact hi j hj⟩
 
 /-- The complex conjugate of a complex Cauchy sequence, as a complex Cauchy sequence. -/
 noncomputable def cau_seq_conj (f : cau_seq ℂ abs) : cau_seq ℂ abs :=