Theorem inner_self_im_zero
Modification history
2023-05-03 18:24
src/analysis/inner_product_space/basic.lean
chore(analysis/inner_product_space/basic): golf, add/merge lemmas (#18928) …
Deleted inner_self_im_zeroView on Github →2023-03-14 13:51
src/analysis/inner_product_space/basic.lean
chore(analysis/inner_product_space/basic): make arguments explicit (#18579) …
Modified inner_self_im_zeroView on Github →