Commit 2023-05-03 18:24 92c69b77

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.