Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-23 02:45 2babfeb0

View on Github →

chore(data/complex/is_R_or_C): squeeze simps (#11251) This PR squeezes most of the simps in is_R_or_C, and updates the module docstring.

Estimated changes

modified theorem is_R_or_C.norm_coe_norm
modified theorem is_R_or_C.I_im'
modified theorem is_R_or_C.I_im
modified theorem is_R_or_C.I_mul_re
modified theorem is_R_or_C.I_re
modified theorem is_R_or_C.I_to_real
modified theorem is_R_or_C.abs_abs
modified theorem is_R_or_C.abs_cast_nat
modified theorem is_R_or_C.abs_conj
modified theorem is_R_or_C.abs_div
modified theorem is_R_or_C.abs_eq_zero
modified theorem is_R_or_C.abs_inv
modified theorem is_R_or_C.abs_mul
modified theorem is_R_or_C.abs_neg
modified theorem is_R_or_C.abs_one
modified theorem is_R_or_C.abs_pos
modified theorem is_R_or_C.abs_to_real
modified theorem is_R_or_C.abs_two
modified theorem is_R_or_C.abs_zero
modified theorem is_R_or_C.bit0_im
modified theorem is_R_or_C.bit0_re
modified theorem is_R_or_C.bit1_im
modified theorem is_R_or_C.bit1_re
modified theorem is_R_or_C.conj_I
modified theorem is_R_or_C.conj_ae_coe
modified theorem is_R_or_C.conj_bit0
modified theorem is_R_or_C.conj_bit1
modified theorem is_R_or_C.conj_cle_apply
modified theorem is_R_or_C.conj_cle_coe
modified theorem is_R_or_C.conj_cle_norm
modified theorem is_R_or_C.conj_eq_re_sub_im
modified theorem is_R_or_C.conj_im
modified theorem is_R_or_C.conj_lie_apply
modified theorem is_R_or_C.conj_neg_I
modified theorem is_R_or_C.conj_of_real
modified theorem is_R_or_C.conj_re
modified theorem is_R_or_C.conj_smul
modified theorem is_R_or_C.conj_to_real
modified theorem is_R_or_C.div_I
modified theorem is_R_or_C.im_clm_apply
modified theorem is_R_or_C.im_clm_coe
modified theorem is_R_or_C.im_lm_coe
modified theorem is_R_or_C.im_to_real
modified theorem is_R_or_C.int_cast_im
modified theorem is_R_or_C.int_cast_re
modified theorem is_R_or_C.inv_I
modified theorem is_R_or_C.inv_im
modified theorem is_R_or_C.inv_re
modified theorem is_R_or_C.mul_im
modified theorem is_R_or_C.mul_re
modified theorem is_R_or_C.nat_cast_im
modified theorem is_R_or_C.nat_cast_re
modified theorem is_R_or_C.norm_conj
modified theorem is_R_or_C.norm_eq_abs
modified theorem is_R_or_C.norm_sq_conj
modified theorem is_R_or_C.norm_sq_div
modified theorem is_R_or_C.norm_sq_eq_zero
modified theorem is_R_or_C.norm_sq_inv
modified theorem is_R_or_C.norm_sq_mul
modified theorem is_R_or_C.norm_sq_neg
modified theorem is_R_or_C.norm_sq_of_real
modified theorem is_R_or_C.norm_sq_one
modified theorem is_R_or_C.norm_sq_pos
modified theorem is_R_or_C.norm_sq_sub
modified theorem is_R_or_C.norm_sq_to_real
modified theorem is_R_or_C.norm_sq_zero
modified theorem is_R_or_C.of_real_add
modified theorem is_R_or_C.of_real_am_coe
modified theorem is_R_or_C.of_real_bit0
modified theorem is_R_or_C.of_real_bit1
modified theorem is_R_or_C.of_real_clm_apply
modified theorem is_R_or_C.of_real_clm_coe
modified theorem is_R_or_C.of_real_clm_norm
modified theorem is_R_or_C.of_real_div
modified theorem is_R_or_C.of_real_eq_zero
modified theorem is_R_or_C.of_real_im
modified theorem is_R_or_C.of_real_int_cast
modified theorem is_R_or_C.of_real_inv
modified theorem is_R_or_C.of_real_li_apply
modified theorem is_R_or_C.of_real_mul
modified theorem is_R_or_C.of_real_mul_im
modified theorem is_R_or_C.of_real_mul_re
modified theorem is_R_or_C.of_real_nat_cast
modified theorem is_R_or_C.of_real_neg
modified theorem is_R_or_C.of_real_one
modified theorem is_R_or_C.of_real_pow
modified theorem is_R_or_C.of_real_prod
modified theorem is_R_or_C.of_real_rat_cast
modified theorem is_R_or_C.of_real_re
modified theorem is_R_or_C.of_real_smul
modified theorem is_R_or_C.of_real_sub
modified theorem is_R_or_C.of_real_sum
modified theorem is_R_or_C.of_real_zero
modified theorem is_R_or_C.of_real_zpow
modified theorem is_R_or_C.one_im
modified theorem is_R_or_C.one_re
modified theorem is_R_or_C.rat_cast_im
modified theorem is_R_or_C.rat_cast_re
modified theorem is_R_or_C.re_add_im
modified theorem is_R_or_C.re_clm_apply
modified theorem is_R_or_C.re_clm_coe
modified theorem is_R_or_C.re_clm_norm
modified theorem is_R_or_C.re_lm_coe
modified theorem is_R_or_C.re_to_real
modified theorem is_R_or_C.smul_im
modified theorem is_R_or_C.smul_re
modified theorem is_R_or_C.zero_re'