Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-11-12 17:08 adb5c2d6

View on Github →

chore(analysis/special_functions/trigonometric/complex): put results about derivatives into a new file (#10156)

Estimated changes

Modified src/analysis/special_functions/trigonometric/arctan.lean

Modified src/analysis/special_functions/trigonometric/complex.lean

deleted theorem complex.continuous_at_tan

deleted theorem complex.deriv_tan

deleted theorem complex.differentiable_at_tan

deleted theorem complex.has_deriv_at_tan

deleted theorem complex.has_strict_deriv_at_tan

deleted theorem complex.tendsto_abs_tan_at_top

deleted theorem complex.tendsto_abs_tan_of_cos_eq_zero

deleted theorem complex.times_cont_diff_at_tan

Created src/analysis/special_functions/trigonometric/complex_deriv.lean

added theorem complex.continuous_at_tan

added theorem complex.deriv_tan

added theorem complex.differentiable_at_tan

added theorem complex.has_deriv_at_tan

added theorem complex.has_strict_deriv_at_tan

added theorem complex.tendsto_abs_tan_at_top

added theorem complex.tendsto_abs_tan_of_cos_eq_zero

added theorem complex.times_cont_diff_at_tan