mathlib

d0c37a11 - feat(analysis/inner_product_space/adjoint): is_self_adjoint_iff_inner… (#12113)

feat(analysis/inner_product_space/adjoint): is_self_adjoint_iff_inner… (#12113) …_map_self_real A linear operator on a complex inner product space is self-adjoint precisely when ⟪T v, v⟫ is real for all v. I am interested in learning style improvements! Co-authored-by: Hans Parshall <hparshall@users.noreply.github.com>