Commit 2025-06-24 19:51 97a13d0d

View on Github →

feat(Analysis/Complex): lemmas involving complex numbers and IsSelfAdjoint (#26034) This PR adds several lemmas related to Complex and RCLike, mostly involving self-adjoint elements and the order on complex numbers. This brings the API a bit closer to the style of the CFC API. See #25636 for the original PR.

Estimated changes

Modified Mathlib/Analysis/Complex/Basic.lean

added theorem Complex.im_eq_zero_iff_isSelfAdjoint

added theorem Complex.norm_of_nonneg'

added theorem Complex.ofReal_eq_re_of_isSelfAdjoint

added theorem Complex.re_eq_ofReal_of_isSelfAdjoint

added theorem Complex.re_le_re

added theorem Complex.re_nonneg_iff_nonneg

added theorem RCLike.ofReal_eq_complex_ofReal

Modified Mathlib/Analysis/RCLike/Basic.lean

added theorem RCLike.im_eq_zero_iff_isSelfAdjoint

added theorem RCLike.im_le_neg_norm_iff_eq_neg_I_mul_norm

modified theorem RCLike.is_real_TFAE

added theorem RCLike.norm_le_im_iff_eq_I_mul_norm

added theorem RCLike.norm_le_re_iff_eq_norm

added theorem RCLike.norm_of_nonneg'

added theorem RCLike.ofReal_eq_re_of_isSelfAdjoint

added theorem RCLike.re_eq_ofReal_of_isSelfAdjoint

added theorem RCLike.re_le_neg_norm_iff_eq_neg_norm

added theorem RCLike.re_le_re

added theorem RCLike.re_monotone

added theorem RCLike.re_nonneg_of_nonneg