Commit 2023-05-18 06:07 a7d75775

View on Github →

port: Analysis.SpecialFunctions.Complex.Log (#4060)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/SpecialFunctions/Complex/Log.lean

added theorem Complex.continuousWithinAt_log_of_re_neg_of_im_zero

added theorem Complex.countable_preimage_exp

added theorem Complex.exp_eq_exp_iff_exists_int

added theorem Complex.exp_eq_exp_iff_exp_sub_eq_one

added theorem Complex.exp_eq_one_iff

added theorem Complex.exp_inj_of_neg_pi_lt_of_le_pi

added theorem Complex.exp_log

added theorem Complex.log_I

added theorem Complex.log_conj

added theorem Complex.log_conj_eq_ite

added theorem Complex.log_exp

added theorem Complex.log_im

added theorem Complex.log_im_le_pi

added theorem Complex.log_inv

added theorem Complex.log_inv_eq_ite

added theorem Complex.log_mul_of_real

added theorem Complex.log_neg_I

added theorem Complex.log_neg_one

added theorem Complex.log_of_real_mul

added theorem Complex.log_of_real_re

added theorem Complex.log_one

added theorem Complex.log_re

added theorem Complex.log_zero

added theorem Complex.map_exp_comap_re_atBot

added theorem Complex.map_exp_comap_re_atTop

added theorem Complex.neg_pi_lt_log_im

added theorem Complex.of_real_log

added theorem Complex.range_exp

added theorem Complex.tendsto_log_nhdsWithin_im_neg_of_re_neg_of_im_zero

added theorem Complex.tendsto_log_nhdsWithin_im_nonneg_of_re_neg_of_im_zero

added theorem Complex.two_pi_I_ne_zero

added theorem Continuous.clog

added theorem ContinuousAt.clog

added theorem ContinuousOn.clog

added theorem ContinuousWithinAt.clog

added theorem Filter.Tendsto.clog

added theorem continuousAt_clog