Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-11-11 14:48 4df3cd76

View on Github →

chore(analysis/special_functions/complex/log): move results about derivatives to a new file (#10117)

Estimated changes

added theorem continuous_at_clog
deleted theorem differentiable.clog
deleted theorem differentiable_at.clog
deleted theorem differentiable_on.clog
deleted theorem has_deriv_at.clog
deleted theorem has_deriv_at.clog_real
deleted theorem has_deriv_within_at.clog
deleted theorem has_fderiv_at.clog
deleted theorem has_fderiv_within_at.clog
deleted theorem has_strict_deriv_at.clog
deleted theorem has_strict_fderiv_at.clog
added theorem differentiable.clog
added theorem differentiable_at.clog
added theorem differentiable_on.clog
added theorem has_deriv_at.clog
added theorem has_deriv_at.clog_real
added theorem has_fderiv_at.clog