Commit 2023-10-31 13:19 c13d8d61

View on Github →

feat(Data/Complex): add lemmas like re_eq_abs (#8025)

Estimated changes

Modified Mathlib/Data/Complex/Basic.lean

added theorem Complex.abs_im_eq_abs

added theorem Complex.abs_re_eq_abs

Modified Mathlib/Data/Complex/Order.lean

deleted theorem Complex.eq_re_ofReal_le

added theorem Complex.eq_re_of_ofReal_le

added theorem Complex.neg_re_eq_abs

added theorem Complex.re_eq_abs

added theorem Complex.re_eq_neg_abs