Theorem real.deriv_tan_of_mem_Ioo
Modification history
2020-12-22 17:05
src/analysis/special_functions/trigonometric.lean
chore(analysis/special_functions/trigonometric): review continuity of `tan` (#5429) …
Deleted real.deriv_tan_of_mem_IooView on Github →