Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-11-03 17:56 8f7ffec9

View on Github →

chore(analysis/special_functions/trigonometric/inverse): move results about derivatives to a new file (#10110) This is part of a refactor of the analysis/special_functions folder, in which I will isolate all lemmas about derivatives. The result will be a definition of Lp spaces that does not import derivatives.

Estimated changes

deleted theorem real.deriv_arccos
deleted theorem real.deriv_arcsin
deleted theorem real.deriv_arcsin_aux
deleted theorem real.has_deriv_at_arccos
deleted theorem real.has_deriv_at_arcsin
added theorem real.deriv_arccos
added theorem real.deriv_arcsin
added theorem real.deriv_arcsin_aux
modified theorem complex.conj_bit0
modified theorem complex.conj_bit1
modified theorem complex.conj_of_real