refactor(data/complex/*): replace complex.conj and is_R_or_C.conj…

… with star (#9640)

This PR replaces `complex.conj` and `is_R_or_C.conj` by the star operation defined in `algebra/star`. Both of these are replaced with `star_ring_aut`, which is also made available under the notation `conj` defined in the locale `complex_conjugate`. This effectively also upgrades conj from a `ring_hom` to a `ring_aut`.

Fixes #9421

src/algebra/star/basic.lean

@@ -211,13 +211,28 @@ def star_ring_equiv [semiring R] [star_ring R] : R ≃+* Rᵒᵖ :=
   ..star_add_equiv.trans (opposite.op_add_equiv : R ≃+ Rᵒᵖ),
   ..star_mul_equiv}
 
-/-- `star` as a `ring_aut` for commutative `R`. -/
-@[simps apply]
+/-- `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` -/
 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
+
+/-- This is not a simp lemma, since we usually want simp to keep `star_ring_aut` 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
+
+@[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
+
+-- 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
+
 @[simp] lemma star_inv' [division_ring R] [star_ring R] (x : R) : star (x⁻¹) = (star x)⁻¹ :=
 op_injective $
   ((star_ring_equiv : R ≃+* Rᵒᵖ).to_ring_hom.map_inv x).trans (op_inv (star x)).symm

src/analysis/complex/basic.lean

@@ -33,6 +33,8 @@ noncomputable theory
 
 namespace complex
 
+open_locale complex_conjugate
+
 instance : has_norm ℂ := ⟨abs⟩
 
 instance : normed_group ℂ :=
@@ -140,14 +142,14 @@ def conj_lie : ℂ ≃ₗᵢ[ℝ] ℂ := ⟨conj_ae.to_linear_equiv, abs_conj⟩
 
 lemma isometry_conj : isometry (conj : ℂ → ℂ) := conj_lie.isometry
 
-@[continuity] lemma continuous_conj : continuous conj := conj_lie.continuous
+@[continuity] lemma continuous_conj : continuous (conj : ℂ → ℂ) := conj_lie.continuous
 
 /-- Continuous linear equiv version of the conj function, from `ℂ` to `ℂ`. -/
 def conj_cle : ℂ ≃L[ℝ] ℂ := conj_lie
 
 @[simp] lemma conj_cle_coe : conj_cle.to_linear_equiv = conj_ae.to_linear_equiv := rfl
 
-@[simp] lemma conj_cle_apply (z : ℂ) : conj_cle z = z.conj := rfl
+@[simp] lemma conj_cle_apply (z : ℂ) : conj_cle z = conj z := rfl
 
 @[simp] lemma conj_cle_norm : ∥(conj_cle : ℂ →L[ℝ] ℂ)∥ = 1 :=
 conj_lie.to_linear_isometry.norm_to_continuous_linear_map
@@ -171,7 +173,6 @@ def of_real_clm : ℝ →L[ℝ] ℂ := of_real_li.to_continuous_linear_map
 noncomputable instance : is_R_or_C ℂ :=
 { re := ⟨complex.re, complex.zero_re, complex.add_re⟩,
   im := ⟨complex.im, complex.zero_im, complex.add_im⟩,
-  conj := complex.conj,
   I := complex.I,
   I_re_ax := by simp only [add_monoid_hom.coe_mk, complex.I_re],
   I_mul_I_ax := by simp only [complex.I_mul_I, eq_self_iff_true, or_true],
@@ -183,8 +184,8 @@ noncomputable instance : is_R_or_C ℂ :=
                                       complex.coe_algebra_map, complex.of_real_eq_coe],
   mul_re_ax := λ z w, by simp only [complex.mul_re, add_monoid_hom.coe_mk],
   mul_im_ax := λ z w, by simp only [add_monoid_hom.coe_mk, complex.mul_im],
-  conj_re_ax := λ z, by simp only [ring_hom.coe_mk, add_monoid_hom.coe_mk, complex.conj_re],
-  conj_im_ax := λ z, by simp only [ring_hom.coe_mk, complex.conj_im, add_monoid_hom.coe_mk],
+  conj_re_ax := λ z, rfl,
+  conj_im_ax := λ z, rfl,
   conj_I_ax := by simp only [complex.conj_I, ring_hom.coe_mk],
   norm_sq_eq_def_ax := λ z, by simp only [←complex.norm_sq_eq_abs, ←complex.norm_sq_apply,
     add_monoid_hom.coe_mk, complex.norm_eq_abs],
@@ -228,14 +229,12 @@ namespace is_R_or_C
 
 local notation `reC` := @is_R_or_C.re ℂ _
 local notation `imC` := @is_R_or_C.im ℂ _
-local notation `conjC` := @is_R_or_C.conj ℂ _
 local notation `IC` := @is_R_or_C.I ℂ _
 local notation `absC` := @is_R_or_C.abs ℂ _
 local notation `norm_sqC` := @is_R_or_C.norm_sq ℂ _
 
 @[simp] lemma re_to_complex {x : ℂ} : reC x = x.re := rfl
 @[simp] lemma im_to_complex {x : ℂ} : imC x = x.im := rfl
-@[simp] lemma conj_to_complex {x : ℂ} : conjC x = x.conj := rfl
 @[simp] lemma I_to_complex : IC = complex.I := rfl
 @[simp] lemma norm_sq_to_complex {x : ℂ} : norm_sqC x = complex.norm_sq x :=
 by simp [is_R_or_C.norm_sq, complex.norm_sq]

src/analysis/complex/circle.lean

@@ -33,6 +33,7 @@ is the kernel of the homomorphism `complex.norm_sq` from `ℂ` to `ℝ`.
 noncomputable theory
 
 open complex metric
+open_locale complex_conjugate
 
 /-- The unit circle in `ℂ`, here given the structure of a submonoid of `ℂ`. -/
 def circle : submonoid ℂ :=
@@ -55,12 +56,12 @@ lemma circle_def : ↑circle = {z : ℂ | abs z = 1} := by { ext, simp }
 lemma nonzero_of_mem_circle (z : circle) : (z:ℂ) ≠ 0 := nonzero_of_mem_unit_sphere z
 
 instance : group circle :=
-{ inv := λ z, ⟨conj z, by simp⟩,
+{ inv := λ z, ⟨conj (z : ℂ), by simp⟩,
   mul_left_inv := λ z, subtype.ext $ by { simp [has_inv.inv, ← norm_sq_eq_conj_mul_self,
     ← mul_self_abs] },
   .. circle.to_monoid }
 
-lemma coe_inv_circle_eq_conj (z : circle) : ↑(z⁻¹) = conj z := rfl
+lemma coe_inv_circle_eq_conj (z : circle) : ↑(z⁻¹) = (conj : ring_aut ℂ) z := rfl
 
 @[simp] lemma coe_inv_circle (z : circle) : ↑(z⁻¹) = (z : ℂ)⁻¹ :=
 begin

src/analysis/complex/conformal.lean

@@ -32,6 +32,7 @@ this file.
 noncomputable theory
 
 open complex continuous_linear_map
+open_locale complex_conjugate
 
 lemma is_conformal_map_conj : is_conformal_map (conj_lie : ℂ →L[ℝ] ℂ) :=
 conj_lie.to_linear_isometry.is_conformal_map

src/analysis/complex/isometry.lean

@@ -25,6 +25,7 @@ The proof of `linear_isometry_complex_aux` is separated in the following parts:
 noncomputable theory
 
 open complex
+open_locale complex_conjugate
 
 local notation `|` x `|` := complex.abs x
 
@@ -59,7 +60,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_hom.map_one, mul_one] at h1,
+  rw [rotation_apply, ring_equiv.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
@@ -99,11 +100,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 [conj.map_sub, conj.map_sub] at this,
+  rw [ring_equiv.map_sub, ring_equiv.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_hom.map_one, 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 [add_sub, sub_left_inj] at this,
   rw [add_comm, ←this, add_comm],
 end

src/analysis/complex/real_deriv.lean

@@ -120,6 +120,7 @@ end real_deriv_of_complex
 section conformality
 /-! ### Conformality of real-differentiable complex maps -/
 open complex continuous_linear_map
+open_locale complex_conjugate
 
 variables
 

src/analysis/fourier.lean

@@ -54,7 +54,7 @@ as Parseval's formula.
 -/
 
 noncomputable theory
-open_locale ennreal
+open_locale ennreal complex_conjugate
 open topological_space continuous_map measure_theory measure_theory.measure algebra submodule set
 
 local attribute [instance] fact_one_le_two_ennreal
@@ -91,7 +91,7 @@ continuous maps from `circle` to `ℂ`. -/
 
 @[simp] lemma fourier_zero {z : circle} : fourier 0 z = 1 := rfl
 
-@[simp] lemma fourier_neg {n : ℤ} {z : circle} : fourier (-n) z = complex.conj (fourier n z) :=
+@[simp] lemma fourier_neg {n : ℤ} {z : circle} : fourier (-n) z = conj (fourier n z) :=
 by simp [← coe_inv_circle_eq_conj z]
 
 @[simp] lemma fourier_add {m n : ℤ} {z : circle} :
@@ -141,7 +141,7 @@ begin
       simp },
     exact subset_adjoin ⟨-n, rfl⟩ },
   { intros c,
-    exact fourier_subalgebra.algebra_map_mem (complex.conj c) },
+    exact fourier_subalgebra.algebra_map_mem (conj c) },
   { intros f g hf hg,
     convert fourier_subalgebra.add_mem hf hg,
     exact alg_hom.map_add _ f g, },
@@ -199,7 +199,7 @@ begin
   rw continuous_map.inner_to_Lp haar_circle (fourier i) (fourier j),
   split_ifs,
   { simp [h, is_probability_measure.measure_univ, ← fourier_neg, ← fourier_add, -fourier_to_fun] },
-  simp only [← fourier_add, ← fourier_neg, is_R_or_C.conj_to_complex],
+  simp only [← fourier_add, ← fourier_neg],
   have hij : -i + j ≠ 0,
   { rw add_comm,
     exact sub_ne_zero.mpr (ne.symm h) },

src/analysis/inner_product_space/basic.lean

@@ -68,7 +68,7 @@ The Coq code is available at the following address: <http://www.lri.fr/~sboldo/e
 noncomputable theory
 
 open is_R_or_C real filter
-open_locale big_operators classical topological_space
+open_locale big_operators classical topological_space complex_conjugate
 
 variables {𝕜 E F : Type*} [is_R_or_C 𝕜]
 
@@ -151,7 +151,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 := @is_R_or_C.conj 𝕜 _
+local postfix `†`:90 := star_ring_aut
 
 /-- Inner product defined by the `inner_product_space.core` structure. -/
 def to_has_inner : has_inner 𝕜 F := { inner := c.inner }
@@ -176,7 +176,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_hom.map_add]; simp only [inner_conj_sym]
+by rw [←inner_conj_sym, inner_add_left, ring_equiv.map_add]; simp only [inner_conj_sym]
 
 lemma inner_norm_sq_eq_inner_self (x : F) : (norm_sqF x : 𝕜) = ⟪x, x⟫ :=
 begin
@@ -194,13 +194,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_hom.map_mul]
+by rw [←inner_conj_sym, inner_smul_left]; simp only [conj_conj, inner_conj_sym, ring_equiv.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_hom.map_zero]
+by rw [←zero_smul 𝕜 (0 : F), inner_smul_left]; simp only [zero_mul, ring_equiv.map_zero]
 
 lemma inner_zero_right {x : F} : ⟪x, 0⟫ = 0 :=
-by rw [←inner_conj_sym, inner_zero_left]; simp only [ring_hom.map_zero]
+by rw [←inner_conj_sym, inner_zero_left]; simp only [ring_equiv.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 })
@@ -215,7 +215,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_hom.map_neg, inner_conj_sym]
+by rw [←inner_conj_sym, inner_neg_left]; simp only [ring_equiv.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] }
@@ -272,7 +272,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, conj_div, h₁, h₃]
+                  : by field_simp [-mul_re, inner_conj_sym, hT, ring_equiv.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⟫)
@@ -384,15 +384,14 @@ 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 := @is_R_or_C.conj 𝕜 _
-local postfix `⋆`:90 := complex.conj
+local postfix `†`:90 := star_ring_aut
 
 export inner_product_space (norm_sq_eq_inner)
 
 section basic_properties
 
 @[simp] lemma inner_conj_sym (x y : E) : ⟪y, x⟫† = ⟪x, y⟫ := inner_product_space.conj_sym _ _
-lemma real_inner_comm (x y : F) : ⟪y, x⟫_ℝ = ⟪x, y⟫_ℝ := inner_conj_sym x y
+lemma real_inner_comm (x y : F) : ⟪y, x⟫_ℝ = ⟪x, y⟫_ℝ := @inner_conj_sym ℝ _ _ _ x y
 
 lemma inner_eq_zero_sym {x y : E} : ⟪x, y⟫ = 0 ↔ ⟪y, x⟫ = 0 :=
 ⟨λ h, by simp [←inner_conj_sym, h], λ h, by simp [←inner_conj_sym, h]⟩
@@ -406,7 +405,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_hom.map_add], simp only [inner_conj_sym] }
+by { rw [←inner_conj_sym, inner_add_left, ring_equiv.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]
@@ -422,7 +421,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_hom.map_mul, conj_conj, inner_conj_sym]
+by rw [←inner_conj_sym, inner_smul_left, ring_equiv.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⟫ :=
@@ -459,7 +458,7 @@ sesq_form.sum_left (sesq_form_of_inner) _ _ _
 /-- An inner product with a sum on the left, `finsupp` version. -/
 lemma finsupp.sum_inner {ι : Type*} (l : ι →₀ 𝕜) (v : ι → E) (x : E) :
   ⟪l.sum (λ (i : ι) (a : 𝕜), a • v i), x⟫
-  = l.sum (λ (i : ι) (a : 𝕜), (is_R_or_C.conj a) • ⟪v i, x⟫) :=
+  = l.sum (λ (i : ι) (a : 𝕜), (conj a) • ⟪v i, x⟫) :=
 by { convert sum_inner l.support (λ a, l a • v a) x, simp [inner_smul_left, finsupp.sum] }
 
 /-- An inner product with a sum on the right, `finsupp` version. -/
@@ -468,13 +467,13 @@ lemma finsupp.inner_sum {ι : Type*} (l : ι →₀ 𝕜) (v : ι → E) (x : E)
 by { convert inner_sum l.support (λ a, l a • v a) x, simp [inner_smul_right, finsupp.sum] }
 
 @[simp] lemma inner_zero_left {x : E} : ⟪0, x⟫ = 0 :=
-by rw [← zero_smul 𝕜 (0:E), inner_smul_left, ring_hom.map_zero, zero_mul]
+by rw [← zero_smul 𝕜 (0:E), inner_smul_left, ring_equiv.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_hom.map_zero]
+by rw [←inner_conj_sym, inner_zero_left, ring_equiv.map_zero]
 
 lemma inner_re_zero_right {x : E} : re ⟪x, 0⟫ = 0 :=
 by simp only [inner_zero_right, add_monoid_hom.map_zero]
@@ -541,7 +540,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_hom.map_neg, inner_conj_sym]
+by rw [←inner_conj_sym, inner_neg_left]; simp only [ring_equiv.map_neg, inner_conj_sym]
 
 lemma inner_neg_neg {x y : E} : ⟪-x, -y⟫ = ⟪x, y⟫ := by simp
 
@@ -620,7 +619,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, conj_div, h₁, h₃, inner_conj_sym]
+                  : by field_simp [-mul_re, hT, ring_equiv.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⟫)

src/analysis/inner_product_space/dual.lean

@@ -42,7 +42,7 @@ section is_R_or_C
 variables (𝕜 : Type*)
 variables {E : Type*} [is_R_or_C 𝕜] [inner_product_space 𝕜 E]
 local notation `⟪`x`, `y`⟫` := @inner 𝕜 E _ x y
-local postfix `†`:90 := @is_R_or_C.conj 𝕜 _
+local postfix `†`:90 := star_ring_aut
 
 /--
 Given some `x` in an inner product space, we can define its dual as the continuous linear map
@@ -115,7 +115,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, conj_div, conj_conj]
+            : by simp [inner_smul_left, ring_equiv.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

@@ -32,7 +32,7 @@ This is recorded in this file as an inner product space instance on `pi_Lp 2`.
 -/
 
 open real set filter is_R_or_C
-open_locale big_operators uniformity topological_space nnreal ennreal
+open_locale big_operators uniformity topological_space nnreal ennreal complex_conjugate
 
 noncomputable theory
 
@@ -67,7 +67,7 @@ instance pi_Lp.inner_product_space {ι : Type*} [fintype ι] (f : ι → Type*)
   begin
     intros x y,
     unfold inner,
-    rw conj.map_sum,
+    rw ring_equiv.map_sum,
     apply finset.sum_congr rfl,
     rintros z -,
     apply inner_conj_sym,

src/analysis/inner_product_space/projection.lean

@@ -527,7 +527,7 @@ begin
   { intros x hx,
     obtain ⟨c, rfl⟩ := submodule.mem_span_singleton.mp hx,
     have hv : ↑∥v∥ ^ 2 = ⟪v, v⟫ := by { norm_cast, simp [norm_sq_eq_inner] },
-    simp [inner_sub_left, inner_smul_left, inner_smul_right, is_R_or_C.conj_div, mul_comm, hv,
+    simp [inner_sub_left, inner_smul_left, inner_smul_right, ring_equiv.map_div, mul_comm, hv,
       inner_product_space.conj_sym, hv] }
 end