Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-12-28 20:31 64770a89

View on Github →

feat(analysis/calculus/deriv): Prove equivalence of Fréchet derivative and the classical definition (#1834)

  • feat(analysis/calculus/deriv): Prove equivalence of Fréchet derivative and the classical definition
  • Fix a typo
  • Move, change doc, add versions for has_deriv_within_at and has_deriv_at.
  • Fix docstring, remove an unsed argument

Estimated changes

deleted theorem filter.tendsto.congr'r
added theorem filter.tendsto_congr'
added theorem filter.tendsto_congr