mathlib3

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

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.