Commit 2025-02-10 17:54 5060a30b

View on Github →

chore(Data/Complex): declare the Complex norm instance sooner (#21494) Create the file Data/Complex/Norm with the minimal imports so that Complex.norm could be defined and related to Complex.abs. Move to Data/Complex/Norm all the results from Analysis/Complex/Basic.lean, where Complex.norm was defined, that depends only on the imports of Data/Complex/Norm.

Estimated changes

deleted theorem Complex.dist_conj_self
deleted theorem Complex.dist_eq
deleted theorem Complex.dist_eq_re_im
deleted theorem Complex.dist_mk
deleted theorem Complex.dist_of_im_eq
deleted theorem Complex.dist_of_re_eq
deleted theorem Complex.dist_self_conj
deleted theorem Complex.edist_of_im_eq
deleted theorem Complex.edist_of_re_eq
deleted theorem Complex.nndist_conj_self
deleted theorem Complex.nndist_of_im_eq
deleted theorem Complex.nndist_of_re_eq
deleted theorem Complex.nndist_self_conj
deleted theorem Complex.nnnorm_I
deleted theorem Complex.nnnorm_natCast
deleted theorem Complex.nnnorm_nnratCast
deleted theorem Complex.nnnorm_ofNat
deleted theorem Complex.nnnorm_ratCast
deleted theorem Complex.nnnorm_real
deleted theorem Complex.normSq_eq_norm_sq
deleted theorem Complex.norm_I
deleted theorem Complex.norm_eq_abs
deleted theorem Complex.norm_intCast
deleted theorem Complex.norm_natCast
deleted theorem Complex.norm_nnratCast
deleted theorem Complex.norm_ofNat
deleted theorem Complex.norm_ratCast
deleted theorem Complex.norm_real
added theorem Complex.dist_conj_self
added theorem Complex.dist_eq
added theorem Complex.dist_eq_re_im
added theorem Complex.dist_mk
added theorem Complex.dist_of_im_eq
added theorem Complex.dist_of_re_eq
added theorem Complex.dist_self_conj
added theorem Complex.edist_of_im_eq
added theorem Complex.edist_of_re_eq
added theorem Complex.nnnorm_I
added theorem Complex.nnnorm_natCast
added theorem Complex.nnnorm_ofNat
added theorem Complex.nnnorm_ratCast
added theorem Complex.nnnorm_real
added theorem Complex.norm_I
added theorem Complex.norm_eq_abs
added theorem Complex.norm_intCast
added theorem Complex.norm_natCast
added theorem Complex.norm_nnratCast
added theorem Complex.norm_ofNat
added theorem Complex.norm_ratCast
added theorem Complex.norm_real