Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-08-08 19:18 ea772710

View on Github →

chore(analysis/calculus/{f,}deriv): fix, add missing lemmas (#8574)

  • use prod.fst and prod.snd in lemmas like has_fderiv_at_fst;
  • add has_strict_deriv_at.prod, has_strict_fderiv_at.comp_has_strict_deriv_at;
  • use set.maps_to in some lemmas;
  • golf some proofs.

Estimated changes

modified theorem has_fderiv_at_fst
modified theorem has_fderiv_at_snd
modified theorem has_strict_fderiv_at_fst
modified theorem has_strict_fderiv_at_snd