chore(data/is_R_or_C/basic): rename conj_mul_eq_norm_sq_left to `co…

…nj_mul` (#18939)

src/analysis/inner_product_space/basic.lean

@@ -259,7 +259,7 @@ begin
   rw [← @of_real_inj 𝕜, coe_norm_sq_eq_inner_self],
   simp only [inner_sub_sub_self, inner_smul_left, inner_smul_right, conj_of_real, mul_sub,
     ← coe_norm_sq_eq_inner_self x, ← coe_norm_sq_eq_inner_self y],
-  rw [← mul_assoc, mul_conj, is_R_or_C.conj_mul_eq_norm_sq_left, norm_sq_eq_def',
+  rw [← mul_assoc, mul_conj, is_R_or_C.conj_mul, norm_sq_eq_def',
     mul_left_comm, ← inner_conj_symm y, mul_conj, norm_sq_eq_def'],
   push_cast,
   ring
@@ -327,8 +327,7 @@ def to_normed_space : normed_space 𝕜 F :=
 { norm_smul_le := assume r x,
   begin
     rw [norm_eq_sqrt_inner, inner_smul_left, inner_smul_right, ←mul_assoc],
-    rw [is_R_or_C.conj_mul_eq_norm_sq_left, of_real_mul_re, sqrt_mul, ← coe_norm_sq_eq_inner_self,
-      of_real_re],
+    rw [is_R_or_C.conj_mul, of_real_mul_re, sqrt_mul, ← coe_norm_sq_eq_inner_self, of_real_re],
     { simp [sqrt_norm_sq_eq_norm, is_R_or_C.sqrt_norm_sq_eq_norm] },
     { exact norm_sq_nonneg r }
   end }

src/analysis/normed_space/extend.lean

@@ -85,7 +85,7 @@ by simp only [extend_to_𝕜'_apply, map_sub, zero_mul, mul_zero, sub_zero] with
 lemma norm_extend_to_𝕜'_apply_sq (f : F →ₗ[ℝ] ℝ) (x : F) :
   ‖(f.extend_to_𝕜' x : 𝕜)‖ ^ 2 = f (conj (f.extend_to_𝕜' x : 𝕜) • x) :=
 calc ‖(f.extend_to_𝕜' x : 𝕜)‖ ^ 2 = re (conj (f.extend_to_𝕜' x) * f.extend_to_𝕜' x : 𝕜) :
-  by rw [is_R_or_C.conj_mul_eq_norm_sq_left, norm_sq_eq_def', of_real_re]
+  by rw [is_R_or_C.conj_mul, norm_sq_eq_def', of_real_re]
 ... = f (conj (f.extend_to_𝕜' x : 𝕜) • x) :
   by rw [← smul_eq_mul, ← map_smul, extend_to_𝕜'_apply_re]
 

src/data/is_R_or_C/basic.lean

@@ -311,6 +311,8 @@ by simp only [map_add, add_zero, ext_iff, monoid_with_zero_hom.coe_mk,
               mul_neg, add_right_neg, zero_add, norm_sq, mul_comm, and_self,
               neg_neg, mul_zero, sub_eq_neg_add, neg_zero] with is_R_or_C_simps
 
+lemma conj_mul (x : K) : conj x * x = ((norm_sq x) : K) := by rw [mul_comm, mul_conj]
+
 theorem add_conj (z : K) : z + conj z = 2 * (re z) :=
 by simp only [ext_iff, two_mul, map_add, add_zero, of_real_im, conj_im, of_real_re,
               eq_self_iff_true, add_right_neg, conj_re, and_self]
@@ -590,14 +592,6 @@ lemma abs_sq_re_add_conj' (x : K) : (abs (conj x + x))^2 = (re (conj x + x))^2 :
 by simp only [sq, ←norm_sq_eq_abs, norm_sq, map_add, add_zero, monoid_with_zero_hom.coe_mk,
               add_left_neg, mul_zero] with is_R_or_C_simps
 
-lemma conj_mul_eq_norm_sq_left (x : K) : conj x * x = ((norm_sq x) : K) :=
-begin
-  rw ext_iff,
-  refine ⟨by simp only [norm_sq, neg_mul, monoid_with_zero_hom.coe_mk,
-                        sub_neg_eq_add, map_add, sub_zero, mul_zero] with is_R_or_C_simps, _⟩,
-  simp only [mul_comm, mul_neg, add_left_neg] with is_R_or_C_simps
-end
-
 /-! ### Cauchy sequences -/
 
 theorem is_cau_seq_re (f : cau_seq K abs) : is_cau_seq abs' (λ n, re (f n)) :=

src/topology/continuous_function/ideals.lean

@@ -260,7 +260,7 @@ begin
       ext,
       simp only [comp_apply, coe_mk, algebra_map_clm_coe, map_pow, coe_mul, coe_star,
         pi.mul_apply, pi.star_apply, star_def, continuous_map.coe_coe],
-      simpa only [norm_sq_eq_def', conj_mul_eq_norm_sq_left, of_real_pow], }, },
+      simpa only [norm_sq_eq_def', is_R_or_C.conj_mul, of_real_pow], }, },
   /- Get the function `g'` which is guaranteed to exist above. By the extreme value theorem and
   compactness of `t`, there is some `0 < c` such that `c ≤ g' x` for all `x ∈ t`. Then by
   `main_lemma_aux` there is some `g` for which `g * g'` is the desired function. -/