Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-02-13 20:44 56a52403

View on Github →

feat(calculus/fderiv): invariance of fderiv under linear equivs (#1977)

  • feat(calculus/fderiv): invariance of fderiv under linear equivs
  • missing material
  • coherent naming conventions
  • fix build
  • coherent naming conventions
  • yury's comments

Estimated changes

modified theorem fderiv_const
added theorem fderiv_const_apply
deleted theorem fderiv_within_const
added theorem norm_prod_le_iff
added theorem linear_equiv.symm_symm
added theorem continuous_on_congr