Mathlib Changelog
v3
Changelog
About
Github
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
Created
src/data/complex/is_R_or_C.lean
added
theorem
is_R_or_C.I_im
added
theorem
is_R_or_C.I_mul_I
added
theorem
is_R_or_C.I_mul_I_of_nonzero
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_abs_sub_le_abs_sub
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_im_div_abs_le_one
added
theorem
is_R_or_C.abs_im_le_abs
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_nonneg
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_re_div_abs_le_one
added
theorem
is_R_or_C.abs_re_le_abs
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_complex
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.char_zero_R_or_C
added
theorem
is_R_or_C.conj_bijective
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_involutive
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_complex
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.eq_conj_iff_re
added
theorem
is_R_or_C.eq_conj_iff_real
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_sq_le_norm_sq
added
theorem
is_R_or_C.im_to_complex
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.is_cau_seq_abs
added
theorem
is_R_or_C.is_cau_seq_im
added
theorem
is_R_or_C.is_cau_seq_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
def
is_R_or_C.norm_sq
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_eq_abs
added
theorem
is_R_or_C.norm_sq_eq_def'
added
theorem
is_R_or_C.norm_sq_eq_def
added
theorem
is_R_or_C.norm_sq_eq_zero
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_nonneg
added
theorem
is_R_or_C.norm_sq_of_real
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_to_complex
added
theorem
is_R_or_C.norm_sq_to_real
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_eq_zero
added
theorem
is_R_or_C.of_real_fpow
added
def
is_R_or_C.of_real_hom
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_int_cast
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_nat_cast
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_rat_cast
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_to_complex
added
theorem
is_R_or_C.of_real_to_real
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_eq_add_conj
added
theorem
is_R_or_C.re_le_abs
added
theorem
is_R_or_C.re_sq_le_norm_sq
added
theorem
is_R_or_C.re_to_complex
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