chore(analysis/inner_product_space/basic): remove bilin_form_of_real_inner (#15780)

Remove `bilin_form_of_real_inner` and add a remark in the docstring of `sesq_form_of_inner` that for over real spaces the sesquilinear form is by definition a bilinear form.

For this we generalize `is_self_adjoint_iff_bilin_form` from `real` to `is_R_or_C` and slightly generalize `linear_map.is_self_adjoint` and `linear_map.is_adjoint_pair` to allow for conjugate linear maps in the second argument.

Author: mcdoll

src/analysis/inner_product_space/basic.lean

@@ -9,7 +9,6 @@ import analysis.convex.uniform
 import analysis.normed_space.completion
 import analysis.normed_space.bounded_linear_maps
 import analysis.normed_space.banach
-import linear_algebra.bilinear_form
 import linear_algebra.sesquilinear_form
 
 /-!
@@ -428,7 +427,9 @@ lemma real_inner_smul_right {x y : F} {r : ℝ} : ⟪x, r • y⟫_ℝ = r * ⟪
 lemma inner_smul_real_right {x y : E} {r : ℝ} : ⟪x, (r : 𝕜) • y⟫ = r • ⟪x, y⟫ :=
 by { rw [inner_smul_right, algebra.smul_def], refl }
 
-/-- The inner product as a sesquilinear form. -/
+/-- The inner product as a sesquilinear form.
+
+Note that in the case `𝕜 = ℝ` this is a bilinear form. -/
 @[simps]
 def sesq_form_of_inner : E →ₗ[𝕜] E →ₗ⋆[𝕜] 𝕜 :=
 linear_map.mk₂'ₛₗ (ring_hom.id 𝕜) (star_ring_end _)
@@ -438,15 +439,6 @@ linear_map.mk₂'ₛₗ (ring_hom.id 𝕜) (star_ring_end _)
   (λ x y z, inner_add_left)
   (λ r x y, inner_smul_left)
 
-/-- The real inner product as a bilinear form. -/
-@[simps]
-def bilin_form_of_real_inner : bilin_form ℝ F :=
-{ bilin := inner,
-  bilin_add_left := λ x y z, inner_add_left,
-  bilin_smul_left := λ a x y, inner_smul_left,
-  bilin_add_right := λ x y z, inner_add_right,
-  bilin_smul_right := λ a x y, inner_smul_right }
-
 /-- An inner product with a sum on the left. -/
 lemma sum_inner {ι : Type*} (s : finset ι) (f : ι → E) (x : E) :
   ⟪∑ i in s, f i, x⟫ = ∑ i in s, ⟪f i, x⟫ := (sesq_form_of_inner x).map_sum

src/analysis/inner_product_space/symmetric.lean

@@ -49,12 +49,12 @@ section real
 
 variables
 
--- Todo: Generalize this to `is_R_or_C`.
-/-- An operator `T` on a `ℝ`-inner product space is symmetric if and only if it is
-`bilin_form.is_self_adjoint` with respect to the bilinear form given by the inner product. -/
-lemma is_symmetric_iff_bilin_form (T : E' →ₗ[ℝ] E') :
-  is_symmetric T ↔ bilin_form_of_real_inner.is_self_adjoint T :=
-by simp [is_symmetric, bilin_form.is_self_adjoint, bilin_form.is_adjoint_pair]
+/-- An operator `T` on an inner product space is symmetric if and only if it is
+`linear_map.is_self_adjoint` with respect to the sesquilinear form given by the inner product. -/
+lemma is_symmetric_iff_sesq_form (T : E →ₗ[𝕜] E) :
+  T.is_symmetric ↔
+  @linear_map.is_self_adjoint 𝕜 E _ _ _ (star_ring_end 𝕜) sesq_form_of_inner T :=
+⟨λ h x y, (h y x).symm, λ h x y, (h y x).symm⟩
 
 end real
 

src/linear_algebra/sesquilinear_form.lean

@@ -387,7 +387,8 @@ variables [comm_semiring R]
 variables [add_comm_monoid M] [module R M]
 variables [add_comm_monoid M₁] [module R M₁]
 variables [add_comm_monoid M₂] [module R M₂]
-variables {B F : M →ₗ[R] M →ₗ[R] R} {B' : M₁ →ₗ[R] M₁ →ₗ[R] R} {B'' : M₂ →ₗ[R] M₂ →ₗ[R] R}
+variables {I : R →+* R}
+variables {B F : M →ₗ[R] M →ₛₗ[I] R} {B' : M₁ →ₗ[R] M₁ →ₛₗ[I] R} {B'' : M₂ →ₗ[R] M₂ →ₛₗ[I] R}
 variables {f f' : M →ₗ[R] M₁} {g g' : M₁ →ₗ[R] M}
 
 variables (B B' f g)
@@ -455,7 +456,8 @@ section add_comm_monoid
 
 variables [comm_semiring R]
 variables [add_comm_monoid M] [module R M]
-variables (B F : M →ₗ[R] M →ₗ[R] R)
+variables {I : R →+* R}
+variables (B F : M →ₗ[R] M →ₛₗ[I] R)
 
 /-- The condition for an endomorphism to be "self-adjoint" with respect to a pair of bilinear forms
 on the underlying module. In the case that these two forms are identical, this is the usual concept