Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-02-02 14:43 6633a70e

View on Github →

feat(analysis/normed_space/inner_product): remove unnecessary nonneg_im field (#5999) The nonneg_im property already follows from conj_sym.

Estimated changes

Modified src/analysis/normed_space/inner_product.lean

modified theorem inner_conj_sym

modified theorem inner_product_space.of_core.inner_self_im_zero

modified theorem inner_product_space.of_core.inner_self_nonneg_im

modified theorem inner_self_im_zero

modified theorem inner_self_nonneg_im

Modified src/analysis/quaternion.lean

Modified src/data/complex/is_R_or_C.lean

added theorem is_R_or_C.conj_I

added theorem is_R_or_C.im_eq_conj_sub