mathlib
6633a70e - feat(analysis/normed_space/inner_product): remove unnecessary `nonneg_im` field (#5999)

Commit
4 years ago
feat(analysis/normed_space/inner_product): remove unnecessary `nonneg_im` field (#5999) The `nonneg_im` property already follows from `conj_sym`.
Author
Parents
Loading