Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-11-27 19:49 198fb09d

View on Github →

feat(analysis/complex/exponential): derivatives (#1695)

  • feat(analysis/complex/exponential): derivatives
  • nhds
  • nhds
  • remove omega
  • remove set_option
  • simp attributes, field type
  • restrict scalar
  • staging
  • complete proof
  • staging
  • cleanup
  • staging
  • cleanup
  • docstring
  • docstring
  • reviewer's comments
  • real derivatives of exp, sin, cos, sinh, cosh
  • fix build
  • remove priority
  • better proofs

Estimated changes

modified theorem asymptotics.is_O_mul
modified theorem asymptotics.is_O_smul
modified theorem asymptotics.is_o_mul
modified theorem asymptotics.is_o_mul_left
modified theorem asymptotics.is_o_mul_right
modified theorem asymptotics.is_o_smul
modified theorem deriv_congr_of_mem_nhds
modified theorem deriv_within_inter
modified theorem has_deriv_within_at_inter
added theorem complex.deriv_cos
added theorem complex.deriv_cosh
added theorem complex.deriv_exp
added theorem complex.deriv_sin
added theorem complex.deriv_sinh
added theorem real.deriv_cos
added theorem real.deriv_cosh
added theorem real.deriv_exp
added theorem real.deriv_sin
added theorem real.deriv_sinh
added theorem real.has_deriv_at_cos
added theorem real.has_deriv_at_cosh
added theorem real.has_deriv_at_exp
added theorem real.has_deriv_at_sin
added theorem real.has_deriv_at_sinh