Commit 2023-03-15 14:32 a3786508
View on Github →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.
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.