Commit 2022-10-26 06:04 ec3c1f27

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.