Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-11-15 17:27 d5d60719

View on Github →

chore(analysis/special_functions/trigonometric/arctan): put lemmas about derivatives into a new file (#10157)

Estimated changes

deleted theorem deriv_arctan
deleted theorem deriv_within_arctan
deleted theorem differentiable.arctan
deleted theorem differentiable_at.arctan
deleted theorem differentiable_on.arctan
deleted theorem fderiv_arctan
deleted theorem fderiv_within_arctan
deleted theorem has_deriv_at.arctan
deleted theorem has_fderiv_at.arctan
deleted theorem real.continuous_at_tan
deleted theorem real.deriv_arctan
deleted theorem real.deriv_tan
deleted theorem real.has_deriv_at_arctan
deleted theorem real.has_deriv_at_tan
deleted theorem times_cont_diff.arctan
deleted theorem times_cont_diff_at.arctan
deleted theorem times_cont_diff_on.arctan
added theorem deriv_arctan
added theorem deriv_within_arctan
added theorem differentiable.arctan
added theorem fderiv_arctan
added theorem fderiv_within_arctan
added theorem has_deriv_at.arctan
added theorem has_fderiv_at.arctan
added theorem real.continuous_at_tan
added theorem real.deriv_arctan
added theorem real.deriv_tan
added theorem real.has_deriv_at_tan
added theorem times_cont_diff.arctan