Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-08-30 05:38 ffce8f67

View on Github →

feat(data/complex/is_R_or_C): add typeclass for real or complex (#3934)

Estimated changes

added theorem is_R_or_C.I_im
added theorem is_R_or_C.I_mul_I
added theorem is_R_or_C.I_re
added theorem is_R_or_C.I_to_complex
added theorem is_R_or_C.I_to_real
added theorem is_R_or_C.abs_abs
added theorem is_R_or_C.abs_add
added theorem is_R_or_C.abs_cast_nat
added theorem is_R_or_C.abs_conj
added theorem is_R_or_C.abs_div
added theorem is_R_or_C.abs_eq_zero
added theorem is_R_or_C.abs_inv
added theorem is_R_or_C.abs_mul
added theorem is_R_or_C.abs_ne_zero
added theorem is_R_or_C.abs_neg
added theorem is_R_or_C.abs_nonneg
added theorem is_R_or_C.abs_of_nat
added theorem is_R_or_C.abs_of_real
added theorem is_R_or_C.abs_one
added theorem is_R_or_C.abs_pos
added theorem is_R_or_C.abs_sub
added theorem is_R_or_C.abs_sub_le
added theorem is_R_or_C.abs_to_real
added theorem is_R_or_C.abs_two
added theorem is_R_or_C.abs_zero
added theorem is_R_or_C.add_conj
added theorem is_R_or_C.bit0_im
added theorem is_R_or_C.bit0_re
added theorem is_R_or_C.bit1_im
added theorem is_R_or_C.bit1_re
added theorem is_R_or_C.conj_bit0
added theorem is_R_or_C.conj_bit1
added theorem is_R_or_C.conj_conj
added theorem is_R_or_C.conj_eq_zero
added theorem is_R_or_C.conj_im
added theorem is_R_or_C.conj_inj
added theorem is_R_or_C.conj_neg_I
added theorem is_R_or_C.conj_of_real
added theorem is_R_or_C.conj_re
added theorem is_R_or_C.conj_to_real
added theorem is_R_or_C.div_I
added theorem is_R_or_C.div_im
added theorem is_R_or_C.div_re
added theorem is_R_or_C.ext
added theorem is_R_or_C.ext_iff
added theorem is_R_or_C.im_le_abs
added theorem is_R_or_C.im_to_real
added theorem is_R_or_C.int_cast_im
added theorem is_R_or_C.int_cast_re
added theorem is_R_or_C.inv_I
added theorem is_R_or_C.inv_def
added theorem is_R_or_C.inv_im
added theorem is_R_or_C.inv_re
added theorem is_R_or_C.mul_conj
added theorem is_R_or_C.mul_im
added theorem is_R_or_C.mul_re
added theorem is_R_or_C.mul_self_abs
added theorem is_R_or_C.nat_cast_im
added theorem is_R_or_C.nat_cast_re
added theorem is_R_or_C.norm_sq_add
added theorem is_R_or_C.norm_sq_conj
added theorem is_R_or_C.norm_sq_div
added theorem is_R_or_C.norm_sq_inv
added theorem is_R_or_C.norm_sq_mul
added theorem is_R_or_C.norm_sq_neg
added theorem is_R_or_C.norm_sq_one
added theorem is_R_or_C.norm_sq_pos
added theorem is_R_or_C.norm_sq_sub
added theorem is_R_or_C.norm_sq_zero
added theorem is_R_or_C.of_real_add
added theorem is_R_or_C.of_real_alg
added theorem is_R_or_C.of_real_bit0
added theorem is_R_or_C.of_real_bit1
added theorem is_R_or_C.of_real_div
added theorem is_R_or_C.of_real_fpow
added theorem is_R_or_C.of_real_im
added theorem is_R_or_C.of_real_inj
added theorem is_R_or_C.of_real_inv
added theorem is_R_or_C.of_real_mul
added theorem is_R_or_C.of_real_neg
added theorem is_R_or_C.of_real_one
added theorem is_R_or_C.of_real_pow
added theorem is_R_or_C.of_real_re
added theorem is_R_or_C.of_real_sub
added theorem is_R_or_C.of_real_zero
added theorem is_R_or_C.one_im
added theorem is_R_or_C.one_re
added theorem is_R_or_C.rat_cast_im
added theorem is_R_or_C.rat_cast_re
added theorem is_R_or_C.re_add_im
added theorem is_R_or_C.re_le_abs
added theorem is_R_or_C.re_to_real
added theorem is_R_or_C.smul_im'
added theorem is_R_or_C.smul_im
added theorem is_R_or_C.smul_re'
added theorem is_R_or_C.smul_re
added theorem is_R_or_C.sub_conj
added theorem is_R_or_C.two_ne_zero
added theorem is_R_or_C.zero_im
added theorem is_R_or_C.zero_re