Commit 2023-12-17 07:58 b835302c

View on Github →

feat: Add congr_mfderiv lemmas mirroring congr_fderiv (#9066) Add convenience lemmas

  • HasMFDerivAt.congr_mfderiv
  • HasMFDerivWithinAt.congr_mfderiv These mirror the already existing
  • HasFDerivAt.congr_fderiv
  • HasFDerivWithinAt.congr_fderiv

Estimated changes