Commit 2024-10-13 23:54 d990505b

View on Github →

chore: rename Complex.ofReal' to Complex.ofReal (#17650) That's already how it was called in lemma names. Rename the existing Complex.ofReal to Complex.ofRealHom

Estimated changes

modified theorem Complex.im_mul_ofReal
modified theorem Complex.im_ofReal_mul
modified theorem Complex.inv_im
modified theorem Complex.inv_re
deleted def Complex.ofReal'
modified def Complex.ofReal
modified theorem Complex.ofReal_comp_add
modified theorem Complex.ofReal_comp_mul
modified theorem Complex.ofReal_comp_neg
modified theorem Complex.ofReal_comp_nsmul
modified theorem Complex.ofReal_comp_pow
modified theorem Complex.ofReal_comp_sub
modified theorem Complex.ofReal_comp_zsmul
modified theorem Complex.ofReal_div
deleted theorem Complex.ofReal_eq_coe
modified theorem Complex.ofReal_intCast
modified theorem Complex.ofReal_natCast
modified theorem Complex.ofReal_nnqsmul
modified theorem Complex.ofReal_nnratCast
modified theorem Complex.ofReal_qsmul
modified theorem Complex.ofReal_ratCast
modified theorem Complex.ofReal_zpow
modified theorem Complex.re_mul_ofReal
modified theorem Complex.re_ofReal_mul
modified theorem Complex.monotone_ofReal
modified theorem Complex.real_le_real
modified theorem Complex.real_lt_real