Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-02-09 20:16 d9d56eb3

View on Github →

feat(analysis/special_functions/trigonometric): complex.log is smooth away from (-∞, 0] (#6041)

Estimated changes

added theorem complex.continuous_im
modified theorem complex.continuous_of_real
added theorem complex.continuous_re
added theorem complex.measurable_im
added theorem complex.measurable_re
added theorem complex.arg_eq_pi_iff
added theorem complex.measurable_arg
added theorem complex.measurable_log
added theorem continuous.clog
added theorem continuous_at.clog
added theorem continuous_on.clog
added theorem differentiable.clog
added theorem differentiable_at.clog
added theorem differentiable_on.clog
added theorem filter.tendsto.clog
added theorem has_deriv_at.clog
added theorem has_fderiv_at.clog
added theorem measurable.carg
added theorem measurable.clog
added theorem complex.of_real_def
added theorem complex.exp_im
added theorem complex.exp_re
added theorem set.image_restrict
modified theorem measurable.const_mul
added theorem measurable.div
modified theorem measurable.mul_const
added theorem measurable.sub_const