Commit 2025-02-24 10:06 ee225888

View on Github →

chore(Data/Complex): deprecate Complex.abs (#21995) in this PR:

  • Defines Complex.norm directly
  • Defines Complex.abs as Complex.norm and deprecate it
  • Change Complex.abs to norm in all definitions / statements / proofs
  • Delete Complex.norm_eq_abs and the file Data.Complex.Abs (its results are moved as deprecated aliases in Data.Complex.Norm)
  • Change the name of all results which refer to Complex.abs to use norm instead and deprecate the original names

Estimated changes

deleted theorem Complex.abs_add_eq
deleted theorem Complex.abs_add_eq_iff
deleted theorem Complex.abs_sub_eq
deleted theorem Complex.abs_sub_eq_iff
added theorem Complex.norm_add_eq
added theorem Complex.norm_sub_eq
deleted theorem Complex.abs_tprod
deleted theorem Complex.continuous_abs
deleted theorem Complex.hasProd_abs
deleted theorem Complex.multipliable_abs
deleted theorem Circle.abs_coe
modified theorem Circle.normSq_coe
added theorem Circle.norm_coe
modified theorem Complex.UnitDisc.coe_mk
modified def Complex.UnitDisc.mk
modified theorem Complex.UnitDisc.mk_coe
modified theorem Complex.UnitDisc.mk_neg
deleted theorem Orientation.abs_kahler
modified theorem Orientation.norm_kahler
deleted theorem Complex.abs_eq_one_iff'
deleted theorem Complex.abs_eq_one_iff
deleted theorem Complex.abs_mul_cos_arg
deleted theorem Complex.abs_mul_sin_arg
modified theorem Complex.arg_of_im_neg
modified theorem Complex.arg_of_im_pos
modified theorem Complex.arg_of_re_nonneg
modified theorem Complex.cos_arg
deleted theorem Complex.ext_abs_arg
deleted theorem Complex.ext_abs_arg_iff
added theorem Complex.ext_norm_arg
modified theorem Complex.sin_arg
modified theorem Complex.log_re
deleted theorem Complex.abs_cpow_inv_nat
modified theorem Complex.abs_cpow_inv_two_im
deleted theorem Complex.abs_cpow_le
deleted theorem Complex.abs_cpow_of_imp
deleted theorem Complex.abs_cpow_real
modified theorem Complex.cpow_inv_two_re
modified theorem Complex.cpow_ofReal_im
modified theorem Complex.cpow_ofReal_re
added theorem Complex.norm_cpow_le
added theorem Complex.norm_cpow_real
deleted theorem Complex.abs_I
deleted theorem Complex.abs_add_mul_I
deleted theorem Complex.abs_apply
deleted theorem Complex.abs_conj
deleted theorem Complex.abs_def
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_intCast
deleted theorem Complex.abs_natCast
deleted theorem Complex.abs_ofNat
deleted theorem Complex.abs_ofReal
deleted theorem Complex.abs_prod
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_zpow
deleted theorem Complex.equiv_limAux
deleted theorem Complex.im_le_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_im
deleted theorem Complex.lim_re
deleted theorem Complex.mul_self_abs
deleted theorem Complex.ne_zero_of_re_pos
deleted theorem Complex.normSq_eq_abs
deleted theorem Complex.range_abs
deleted theorem Complex.range_normSq
deleted theorem Complex.re_le_abs
deleted theorem Complex.sq_abs_sub_sq_im
deleted theorem Complex.sq_abs_sub_sq_re
deleted theorem Complex.abs_exp_ofReal
modified def Complex.exp'
modified theorem Complex.exp_bound'
modified theorem Complex.exp_bound
deleted theorem Complex.isCauSeq_abs_exp
modified theorem Complex.isCauSeq_exp
added theorem Complex.abs_im_eq_norm
added theorem Complex.abs_im_le_norm
added theorem Complex.abs_im_lt_norm
added theorem Complex.abs_re_eq_norm
added theorem Complex.abs_re_le_norm
added theorem Complex.abs_re_lt_norm
modified theorem Complex.dist_eq
added theorem Complex.equiv_limAux
added theorem Complex.im_le_norm
added theorem Complex.isCauSeq_conj
added theorem Complex.isCauSeq_im
added theorem Complex.isCauSeq_norm
added theorem Complex.isCauSeq_re
added theorem Complex.lim_conj
added theorem Complex.lim_im
added theorem Complex.lim_norm
added theorem Complex.lim_re
modified theorem Complex.nnnorm_natCast
modified theorem Complex.nnnorm_nnratCast
modified theorem Complex.nnnorm_ofNat
modified theorem Complex.nnnorm_ratCast
modified theorem Complex.nnnorm_real
modified theorem Complex.norm_I
added theorem Complex.norm_add_mul_I
added theorem Complex.norm_conj
added theorem Complex.norm_def
deleted theorem Complex.norm_eq_abs
modified theorem Complex.norm_intCast
modified theorem Complex.norm_natCast
modified theorem Complex.norm_nnratCast
modified theorem Complex.norm_ofNat
modified theorem Complex.norm_ratCast
modified theorem Complex.norm_real
added theorem Complex.range_normSq
added theorem Complex.re_le_norm
deleted theorem Complex.neg_re_eq_abs
added theorem Complex.neg_re_eq_norm
deleted theorem Complex.re_eq_abs
deleted theorem Complex.re_eq_neg_abs
added theorem Complex.re_eq_neg_norm
added theorem Complex.re_eq_norm
deleted theorem Complex.abs_exp
added theorem Complex.norm_exp
deleted theorem abs_circleMap_zero
added theorem norm_circleMap_zero
modified theorem EisensteinSeries.auxbound1
modified theorem EisensteinSeries.auxbound2