Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-07-19 14:09 74754acb

View on Github →

feat(analysis/calculus/times_cont_diff): multiple differentiability (#1226)

  • feat(analysis/calculus/times_cont_diff): multiple differentiability
  • style
  • style
  • style and documentation
  • better wording

Estimated changes

added def iterated_fderiv
added theorem iterated_fderiv_succ
added theorem iterated_fderiv_zero
added theorem times_cont_diff.comp
added theorem times_cont_diff.of_le
added theorem times_cont_diff.prod
added def times_cont_diff
added theorem times_cont_diff_const
added theorem times_cont_diff_fst
added theorem times_cont_diff_id
added theorem times_cont_diff_on_top
added theorem times_cont_diff_snd
added theorem times_cont_diff_succ
added theorem times_cont_diff_top
added theorem times_cont_diff_zero