mathlib

92c69b77 - chore(analysis/inner_product_space/basic): golf, add/merge lemmas (#18928)

chore(analysis/inner_product_space/basic): golf, add/merge lemmas (#18928) - Merge `inner_product_space.of_core.inner_self_nonneg_im` and `inner_product_space.of_core.inner_self_im_zero` into `inner_product_space.of_core.inner_self_im`. - Rename `inner_product_space.of_core.inner_abs_conj_symm` to `inner_product_space.of_core.abs_inner_symm`. - Rename `inner_abs_conj_symm` to `abs_inner_symm`. - Add `inner_product_space.of_core.norm_sq_eq_zero`. - Merge `inner_self_nonneg_im` and `inner_self_im_zero` into `inner_self_im`. - Reorder, golf.