mathlib3

a3786508 - chore(analysis/inner_product_space/basic): add inner_self_ne_zero (#18587)

chore(analysis/inner_product_space/basic): add inner_self_ne_zero (#18587) This result is trivial, but it's presence is consistent with how we have both `norm_ne_zero` and `norm_ne_zero_iff`.