Commit 2023-05-12 05:54 797788a5

View on Github →

feat: port Data.IsROrC.Basic (#3654)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/IsROrC/Attr.lean

Created Mathlib/Data/IsROrC/Basic.lean

added theorem IsROrC.I_im'

added theorem IsROrC.I_im

added theorem IsROrC.I_mul_I

added theorem IsROrC.I_mul_I_of_nonzero

added theorem IsROrC.I_mul_re

added theorem IsROrC.I_re

added theorem IsROrC.I_to_real

added theorem IsROrC.abs_im_div_norm_le_one

added theorem IsROrC.abs_im_le_norm

added theorem IsROrC.abs_re_div_norm_le_one

added theorem IsROrC.abs_re_le_norm

added theorem IsROrC.add_conj

added theorem IsROrC.algebraMap_eq_ofReal

added theorem IsROrC.bit0_im

added theorem IsROrC.bit0_re

added theorem IsROrC.bit1_im

added theorem IsROrC.bit1_re

added def IsROrC.conjAe

added theorem IsROrC.conjAe_coe

added theorem IsROrC.conjCle_apply

added theorem IsROrC.conjCle_coe

added theorem IsROrC.conjLie_apply

added theorem IsROrC.conj_I

added theorem IsROrC.conj_bit0

added theorem IsROrC.conj_bit1

added theorem IsROrC.conj_eq_iff_im

added theorem IsROrC.conj_eq_iff_re

added theorem IsROrC.conj_eq_iff_real

added theorem IsROrC.conj_eq_re_sub_im

added theorem IsROrC.conj_im

added theorem IsROrC.conj_inv

added theorem IsROrC.conj_mul

added theorem IsROrC.conj_neg_I

added theorem IsROrC.conj_ofReal

added theorem IsROrC.conj_re

added theorem IsROrC.conj_smul

added theorem IsROrC.conj_to_real

added theorem IsROrC.continuous_conj

added theorem IsROrC.continuous_im

added theorem IsROrC.continuous_normSq

added theorem IsROrC.continuous_ofReal

added theorem IsROrC.continuous_re

added theorem IsROrC.div_I

added theorem IsROrC.div_im

added theorem IsROrC.div_re

added theorem IsROrC.div_re_ofReal

added theorem IsROrC.ext

added theorem IsROrC.ext_iff

added theorem IsROrC.imClm_apply

added theorem IsROrC.imClm_coe

added def IsROrC.imLm

added theorem IsROrC.imLm_coe

added theorem IsROrC.im_eq_conj_sub

added theorem IsROrC.im_eq_zero_of_le

added theorem IsROrC.im_le_norm

added theorem IsROrC.im_sq_le_normSq

added theorem IsROrC.im_to_real

added theorem IsROrC.intCast_im

added theorem IsROrC.intCast_re

added theorem IsROrC.inv_I

added theorem IsROrC.inv_def

added theorem IsROrC.inv_im

added theorem IsROrC.inv_re

added theorem IsROrC.isCauSeq_im

added theorem IsROrC.isCauSeq_norm

added theorem IsROrC.isCauSeq_re

added theorem IsROrC.is_real_TFAE

added theorem IsROrC.mul_conj

added theorem IsROrC.mul_im

added theorem IsROrC.mul_re

added theorem IsROrC.mul_self_norm

added theorem IsROrC.natCast_im

added theorem IsROrC.natCast_re

added def IsROrC.normSq

added theorem IsROrC.normSq_add

added theorem IsROrC.normSq_apply

added theorem IsROrC.normSq_conj

added theorem IsROrC.normSq_div

added theorem IsROrC.normSq_eq_def'

added theorem IsROrC.normSq_eq_zero

added theorem IsROrC.normSq_inv

added theorem IsROrC.normSq_mul

added theorem IsROrC.normSq_neg

added theorem IsROrC.normSq_nonneg

added theorem IsROrC.normSq_one

added theorem IsROrC.normSq_pos

added theorem IsROrC.normSq_sub

added theorem IsROrC.normSq_to_real

added theorem IsROrC.normSq_zero

added theorem IsROrC.norm_conj

added theorem IsROrC.norm_im_le_norm

added theorem IsROrC.norm_natCast

added theorem IsROrC.norm_ofNat

added theorem IsROrC.norm_ofReal

added theorem IsROrC.norm_of_nonneg

added theorem IsROrC.norm_re_le_norm

added theorem IsROrC.norm_sq_eq_def

added theorem IsROrC.norm_sq_re_add_conj

added theorem IsROrC.norm_sq_re_conj_add

added theorem IsROrC.norm_two

added theorem IsROrC.ofNat_im

added theorem IsROrC.ofNat_mul_im

added theorem IsROrC.ofNat_mul_re

added theorem IsROrC.ofNat_re

added theorem IsROrC.ofRealAm_coe

added theorem IsROrC.ofRealClm_apply

added theorem IsROrC.ofRealClm_coe

added theorem IsROrC.ofRealLi_apply

added theorem IsROrC.ofReal_add

added theorem IsROrC.ofReal_alg

added theorem IsROrC.ofReal_bit0

added theorem IsROrC.ofReal_bit1

added theorem IsROrC.ofReal_div

added theorem IsROrC.ofReal_eq_zero

added theorem IsROrC.ofReal_finsupp_prod

added theorem IsROrC.ofReal_finsupp_sum

added theorem IsROrC.ofReal_im

added theorem IsROrC.ofReal_inj

added theorem IsROrC.ofReal_injective

added theorem IsROrC.ofReal_intCast

added theorem IsROrC.ofReal_inv

added theorem IsROrC.ofReal_mul

added theorem IsROrC.ofReal_mul_im

added theorem IsROrC.ofReal_mul_re

added theorem IsROrC.ofReal_natCast

added theorem IsROrC.ofReal_ne_zero

added theorem IsROrC.ofReal_neg

added theorem IsROrC.ofReal_ofNat

added theorem IsROrC.ofReal_one

added theorem IsROrC.ofReal_pow

added theorem IsROrC.ofReal_prod

added theorem IsROrC.ofReal_ratCast

added theorem IsROrC.ofReal_re

added theorem IsROrC.ofReal_real_eq_id

added theorem IsROrC.ofReal_sub

added theorem IsROrC.ofReal_sum

added theorem IsROrC.ofReal_zero

added theorem IsROrC.ofReal_zpow

added theorem IsROrC.one_im

added theorem IsROrC.one_re

added theorem IsROrC.ratCast_im

added theorem IsROrC.ratCast_re

added theorem IsROrC.reClm_apply

added theorem IsROrC.reClm_coe

added def IsROrC.reLm

added theorem IsROrC.reLm_coe

added theorem IsROrC.re_add_im

added theorem IsROrC.re_eq_add_conj

added theorem IsROrC.re_eq_norm_of_mul_conj

added theorem IsROrC.re_eq_self_of_le

added theorem IsROrC.re_le_norm

added theorem IsROrC.re_sq_le_normSq

added theorem IsROrC.re_to_real

added theorem IsROrC.real_smul_eq_coe_mul

added theorem IsROrC.real_smul_eq_coe_smul

added theorem IsROrC.real_smul_ofReal

added theorem IsROrC.smul_im

added theorem IsROrC.smul_re

added theorem IsROrC.sqrt_normSq_eq_norm

added theorem IsROrC.star_def

added theorem IsROrC.sub_conj

added theorem IsROrC.zero_re'

Modified Mathlib/Mathport/Rename.lean