Commit 2024-01-09 21:58 b8370f89

View on Github →

feat: Basic Complex lemmas (#9527) and rename ofReal_mul_re → re_mul_ofReal, ofReal_mul_im → im_mul_ofReal. From LeanAPAP

Estimated changes

added theorem Complex.abs_add_mul_I
modified theorem Complex.I_ne_zero
added theorem Complex.im_mul_ofReal
added theorem Complex.im_ofReal_mul
deleted theorem Complex.ofReal_mul_im
deleted theorem Complex.ofReal_mul_re
added theorem Complex.ofReal_nsmul
added theorem Complex.ofReal_zsmul
added theorem Complex.re_mul_ofReal
added theorem Complex.re_ofReal_mul
added theorem IsROrC.im_ofReal_mul
deleted theorem IsROrC.ofReal_mul_im
deleted theorem IsROrC.ofReal_mul_re
added theorem IsROrC.re_ofReal_mul