Commit 2023-03-10 12:58 a79a9dc6

View on Github →

feat: port Data.Complex.Basic (#2718)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Complex/Basic.lean

added theorem Complex.AbsTheory.abs_conj

added theorem Complex.ComplexOrder.eq_re_ofReal_le

added theorem Complex.ComplexOrder.le_def

added theorem Complex.ComplexOrder.lt_def

added theorem Complex.ComplexOrder.not_le_iff

added theorem Complex.ComplexOrder.not_le_zero_iff

added theorem Complex.ComplexOrder.not_lt_iff

added theorem Complex.ComplexOrder.not_lt_zero_iff

added theorem Complex.ComplexOrder.real_le_real

added theorem Complex.ComplexOrder.real_lt_real

added theorem Complex.ComplexOrder.zero_le_real

added theorem Complex.ComplexOrder.zero_lt_real

added def Complex.I

added def Complex.Set.reProdIm

added theorem Complex.abs_I

added theorem Complex.abs_abs

added theorem Complex.abs_apply

added theorem Complex.abs_cast_nat

added theorem Complex.abs_conj

added theorem Complex.abs_def

added theorem Complex.abs_im_div_abs_le_one

added theorem Complex.abs_im_le_abs

added theorem Complex.abs_im_lt_abs

added theorem Complex.abs_le_abs_re_add_abs_im

added theorem Complex.abs_le_sqrt_two_mul_max

added theorem Complex.abs_ofReal

added theorem Complex.abs_of_nat

added theorem Complex.abs_pow

added theorem Complex.abs_prod

added theorem Complex.abs_re_div_abs_le_one

added theorem Complex.abs_re_le_abs

added theorem Complex.abs_re_lt_abs

added theorem Complex.abs_two

added theorem Complex.abs_zpow

added theorem Complex.add_conj

added theorem Complex.add_im

added theorem Complex.add_re

added theorem Complex.bit0_im

added theorem Complex.bit0_re

added theorem Complex.bit1_im

added theorem Complex.bit1_re

added theorem Complex.coe_imAddGroupHom

added theorem Complex.coe_reAddGroupHom

added theorem Complex.conj_I

added theorem Complex.conj_bit0

added theorem Complex.conj_bit1

added theorem Complex.conj_im

added theorem Complex.conj_inv

added theorem Complex.conj_neg_I

added theorem Complex.conj_ofReal

added theorem Complex.conj_re

added theorem Complex.div_I

added theorem Complex.div_im

added theorem Complex.div_re

added theorem Complex.eq_conj_iff_im

added theorem Complex.eq_conj_iff_re

added theorem Complex.eq_conj_iff_real

added def Complex.equivRealProd

added theorem Complex.equivRealProd_symm_apply

added theorem Complex.equiv_limAux

added theorem Complex.eta

added theorem Complex.ext

added theorem Complex.ext_iff

added theorem Complex.i_im

added theorem Complex.i_mul

added theorem Complex.i_mul_I

added theorem Complex.i_mul_im

added theorem Complex.i_mul_re

added theorem Complex.i_ne_zero

added theorem Complex.i_pow_bit0

added theorem Complex.i_pow_bit1

added theorem Complex.i_re

added theorem Complex.i_sq

added theorem Complex.i_zpow_bit0

added theorem Complex.i_zpow_bit1

added def Complex.imAddGroupHom

added theorem Complex.im_eq_sub_conj

added theorem Complex.im_le_abs

added theorem Complex.im_sq_le_normSq

added theorem Complex.im_sum

added theorem Complex.im_surjective

added theorem Complex.int_cast_abs

added theorem Complex.int_cast_im

added theorem Complex.int_cast_re

added theorem Complex.inv_I

added theorem Complex.inv_def

added theorem Complex.inv_im

added theorem Complex.inv_re

added theorem Complex.isCauSeq_abs

added theorem Complex.isCauSeq_conj

added theorem Complex.isCauSeq_im

added theorem Complex.isCauSeq_re

added theorem Complex.lim_abs

added theorem Complex.lim_conj

added theorem Complex.lim_eq_lim_im_add_lim_re

added theorem Complex.lim_im

added theorem Complex.lim_re

added theorem Complex.mem_reProdIm

added theorem Complex.mk_eq_add_mul_I

added theorem Complex.mul_I_im

added theorem Complex.mul_I_re

added theorem Complex.mul_conj

added theorem Complex.mul_im

added theorem Complex.mul_re

added theorem Complex.mul_self_abs

added theorem Complex.nat_cast_im

added theorem Complex.nat_cast_re

added theorem Complex.neg_im

added theorem Complex.neg_re

added def Complex.normSq

added theorem Complex.normSq_I

added theorem Complex.normSq_add

added theorem Complex.normSq_add_mul_I

added theorem Complex.normSq_apply

added theorem Complex.normSq_conj

added theorem Complex.normSq_div

added theorem Complex.normSq_eq_abs

added theorem Complex.normSq_eq_conj_mul_self

added theorem Complex.normSq_eq_zero

added theorem Complex.normSq_inv

added theorem Complex.normSq_mk

added theorem Complex.normSq_mul

added theorem Complex.normSq_neg

added theorem Complex.normSq_nonneg

added theorem Complex.normSq_ofReal

added theorem Complex.normSq_one

added theorem Complex.normSq_pos

added theorem Complex.normSq_sub

added theorem Complex.normSq_zero

added def Complex.ofReal'

added def Complex.ofReal

added theorem Complex.ofReal_add

added theorem Complex.ofReal_bit0

added theorem Complex.ofReal_bit1

added theorem Complex.ofReal_def

added theorem Complex.ofReal_div

added theorem Complex.ofReal_eq_coe

added theorem Complex.ofReal_eq_one

added theorem Complex.ofReal_eq_zero

added theorem Complex.ofReal_im

added theorem Complex.ofReal_inj

added theorem Complex.ofReal_injective

added theorem Complex.ofReal_int_cast

added theorem Complex.ofReal_inv

added theorem Complex.ofReal_mul'

added theorem Complex.ofReal_mul

added theorem Complex.ofReal_mul_im

added theorem Complex.ofReal_mul_re

added theorem Complex.ofReal_nat_cast

added theorem Complex.ofReal_ne_one

added theorem Complex.ofReal_ne_zero

added theorem Complex.ofReal_neg

added theorem Complex.ofReal_one

added theorem Complex.ofReal_pow

added theorem Complex.ofReal_prod

added theorem Complex.ofReal_rat_cast

added theorem Complex.ofReal_re

added theorem Complex.ofReal_sub

added theorem Complex.ofReal_sum

added theorem Complex.ofReal_zero

added theorem Complex.ofReal_zpow

added theorem Complex.one_im

added theorem Complex.one_re

added theorem Complex.range_abs

added theorem Complex.range_im

added theorem Complex.range_normSq

added theorem Complex.range_re

added theorem Complex.rat_cast_im

added theorem Complex.rat_cast_re

added def Complex.reAddGroupHom

added theorem Complex.re_add_im

added theorem Complex.re_eq_add_conj

added theorem Complex.re_le_abs

added theorem Complex.re_sq_le_normSq

added theorem Complex.re_sum

added theorem Complex.re_surjective

added theorem Complex.sq_abs

added theorem Complex.sq_abs_sub_sq_im

added theorem Complex.sq_abs_sub_sq_re

added theorem Complex.star_def

added theorem Complex.sub_conj

added theorem Complex.sub_im

added theorem Complex.sub_re

added theorem Complex.zero_im

added theorem Complex.zero_re

added structure Complex