Commit 2023-11-14 03:24 6f8dabb5

View on Github →

chore: split Data.Complex.Basic (#8355)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Complex/Abs.lean

added theorem Complex.AbsTheory.abs_conj

added theorem Complex.abs_I

added theorem Complex.abs_abs

added theorem Complex.abs_apply

added theorem Complex.abs_conj

added theorem Complex.abs_def

added theorem Complex.abs_im_div_abs_le_one

added theorem Complex.abs_im_eq_abs

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_natCast

added theorem Complex.abs_ofNat

added theorem Complex.abs_ofReal

added theorem Complex.abs_pow

added theorem Complex.abs_prod

added theorem Complex.abs_re_div_abs_le_one

added theorem Complex.abs_re_eq_abs

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.equiv_limAux

added theorem Complex.im_le_abs

added theorem Complex.int_cast_abs

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.mul_self_abs

added theorem Complex.normSq_eq_abs

added theorem Complex.range_abs

added theorem Complex.range_normSq

added theorem Complex.re_le_abs

added theorem Complex.sq_abs

added theorem Complex.sq_abs_sub_sq_im

added theorem Complex.sq_abs_sub_sq_re

Modified Mathlib/Data/Complex/Basic.lean

deleted theorem Complex.AbsTheory.abs_conj

deleted theorem Complex.abs_I

deleted theorem Complex.abs_abs

deleted theorem Complex.abs_apply

deleted theorem Complex.abs_conj

deleted theorem Complex.abs_def

deleted theorem Complex.abs_im_div_abs_le_one

deleted theorem Complex.abs_im_eq_abs

deleted theorem Complex.abs_im_le_abs

deleted theorem Complex.abs_im_lt_abs

deleted theorem Complex.abs_le_abs_re_add_abs_im

deleted theorem Complex.abs_le_sqrt_two_mul_max

deleted theorem Complex.abs_natCast

deleted theorem Complex.abs_ofNat

deleted theorem Complex.abs_ofReal

deleted theorem Complex.abs_pow

deleted theorem Complex.abs_prod

deleted theorem Complex.abs_re_div_abs_le_one

deleted theorem Complex.abs_re_eq_abs

deleted theorem Complex.abs_re_le_abs

deleted theorem Complex.abs_re_lt_abs

deleted theorem Complex.abs_two

deleted theorem Complex.abs_zpow

deleted theorem Complex.equiv_limAux

deleted theorem Complex.im_le_abs

deleted theorem Complex.im_sum

deleted theorem Complex.int_cast_abs

deleted theorem Complex.isCauSeq_abs

deleted theorem Complex.isCauSeq_conj

deleted theorem Complex.isCauSeq_im

deleted theorem Complex.isCauSeq_re

deleted theorem Complex.lim_abs

deleted theorem Complex.lim_conj

deleted theorem Complex.lim_eq_lim_im_add_lim_re

deleted theorem Complex.lim_im

deleted theorem Complex.lim_re

deleted theorem Complex.mul_self_abs

deleted theorem Complex.normSq_eq_abs

deleted theorem Complex.ofReal_prod

deleted theorem Complex.ofReal_sum

deleted theorem Complex.range_abs

deleted theorem Complex.range_normSq

deleted theorem Complex.re_le_abs

deleted theorem Complex.re_sum

deleted theorem Complex.sq_abs

deleted theorem Complex.sq_abs_sub_sq_im

deleted theorem Complex.sq_abs_sub_sq_re

Created Mathlib/Data/Complex/BigOperators.lean

added theorem Complex.im_sum

added theorem Complex.ofReal_prod

added theorem Complex.ofReal_sum

added theorem Complex.re_sum

Modified Mathlib/Data/Complex/Exponential.lean

Modified Mathlib/Data/Complex/Module.lean

Modified Mathlib/Data/Complex/Order.lean

Modified Mathlib/NumberTheory/Zsqrtd/GaussianInt.lean