Commit 2025-03-01 19:05 39cd8860

View on Github →

feat(FDeriv/Add): drop unneeded assumptions (#22244)

  • Upgrade const_add and add_const lemmas to @[simp] Iffs, use alias to generate the old lemmas.
    • The order of arguments generated by alias differs from the old one, but the dot notation still works.
  • Drop the unneeded UniqueDiffWithinAt assumptions in fderivWithin_add_const and fderivWithin_const_add.

Estimated changes

modified theorem deriv_const_add'
modified theorem deriv_const_add
added theorem deriv_sub_const_fun
deleted theorem Differentiable.add_const
deleted theorem Differentiable.const_add
modified theorem fderivWithin_add_const
modified theorem fderivWithin_const_add
modified theorem fderivWithin_sub_const