Commit 2023-05-15 21:28 0c891722

View on Github →

feat: port Analysis.Complex.Basic (#3930)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/Complex/Basic.lean

added theorem Complex.antilipschitz_equivRealProd

added theorem Complex.comap_abs_nhds_zero

added def Complex.conjCle

added theorem Complex.conjCle_apply

added theorem Complex.conjCle_coe

added def Complex.conjLie

added theorem Complex.conjLie_apply

added theorem Complex.conjLie_symm

added theorem Complex.conj_tsum

added theorem Complex.continuous_abs

added theorem Complex.continuous_conj

added theorem Complex.continuous_im

added theorem Complex.continuous_normSq

added theorem Complex.continuous_ofReal

added theorem Complex.continuous_re

added theorem Complex.dist_conj_comm

added theorem Complex.dist_conj_conj

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

added def Complex.equivRealProdClm

added theorem Complex.equivRealProd_apply_le'

added theorem Complex.equivRealProd_apply_le

added theorem Complex.hasSum_conj'

added theorem Complex.hasSum_conj

added theorem Complex.hasSum_iff

added theorem Complex.hasSum_im

added theorem Complex.hasSum_ofReal

added theorem Complex.hasSum_re

added def Complex.imClm

added theorem Complex.imClm_apply

added theorem Complex.imClm_coe

added theorem Complex.im_tsum

added theorem Complex.isometry_conj

added theorem Complex.isometry_ofReal

added theorem Complex.lipschitz_equivRealProd

added theorem Complex.nndist_conj_comm

added theorem Complex.nndist_conj_conj

added theorem Complex.nndist_conj_self

added theorem Complex.nndist_of_im_eq

added theorem Complex.nndist_of_re_eq

added theorem Complex.nndist_self_conj

added theorem Complex.nnnorm_eq_one_of_pow_eq_one

added theorem Complex.nnnorm_int

added theorem Complex.nnnorm_nat

added theorem Complex.nnnorm_real

added theorem Complex.norm_eq_abs

added theorem Complex.norm_eq_one_of_pow_eq_one

added theorem Complex.norm_exp_ofReal_mul_I

added theorem Complex.norm_int

added theorem Complex.norm_int_of_nonneg

added theorem Complex.norm_nat

added theorem Complex.norm_rat

added theorem Complex.norm_real

added def Complex.ofRealClm

added theorem Complex.ofRealClm_apply

added theorem Complex.ofRealClm_coe

added def Complex.ofRealLi

added theorem Complex.ofReal_tsum

added def Complex.reClm

added theorem Complex.reClm_apply

added theorem Complex.reClm_coe

added theorem Complex.re_tsum

added theorem Complex.restrictScalars_one_smulRight

added theorem Complex.restrictScalars_one_smul_right'

added theorem Complex.ringHom_eq_id_or_conj_of_continuous

added theorem Complex.ringHom_eq_ofReal_of_continuous

added theorem Complex.summable_conj

added theorem Complex.summable_ofReal

added theorem Complex.tendsto_abs_cocompact_atTop

added theorem Complex.tendsto_normSq_cocompact_atTop

added theorem Complex.uniformEmbedding_equivRealProd

added theorem IsROrC.I_to_complex

added theorem IsROrC.conj_tsum

added theorem IsROrC.hasSum_conj'

added theorem IsROrC.hasSum_conj

added theorem IsROrC.hasSum_iff

added theorem IsROrC.hasSum_im

added theorem IsROrC.hasSum_ofReal

added theorem IsROrC.hasSum_re

added theorem IsROrC.im_eq_complex_im

added theorem IsROrC.im_to_complex

added theorem IsROrC.im_tsum

added theorem IsROrC.normSq_to_complex

added theorem IsROrC.ofReal_tsum

added theorem IsROrC.re_eq_complex_re

added theorem IsROrC.re_to_complex

added theorem IsROrC.re_tsum

added theorem IsROrC.summable_conj

added theorem IsROrC.summable_ofReal