Commit 2024-01-09 14:03 bca393b0

View on Github →

chore(ContDiffAt): fix several names (#9584) Rename

  • Filter.EventuallyEq.iterated_fderiv_within' → Filter.EventuallyEq.iteratedFDerivWithin'
  • contDiffOn_succ_iff_has_fderiv_within → contDiffOn_succ_iff_hasFDerivWithin
  • contDiff_succ_iff_has_fderiv → contDiff_succ_iff_hasFDerivAt

Estimated changes