Commit 2026-10-01 20:33 850d7abd

View on Github →

chore(Calculus/FDeriv/Add): reorganize the file (#44203)

  • split section Add into Add and AddConst, and section Sub into Sub and SubConst, so that each section deals with one operation;
  • move differentiableWithinAt_smul_iff and differentiableAt_smul_iff before the lemmas about fderivWithin/fderiv of c • f. No lemma is added, removed, or restated. Extracted by Claude from a larger refactor written by Yury.

Estimated changes