Commit 2025-05-16 04:21 82462926

View on Github →

chore(Calculus): add Function.const versions of some lemmas (#24756) Rename fun _ ↦ c versions to fun_const.

Estimated changes

modified theorem derivWithin_const
added theorem derivWithin_fun_const
modified theorem fderivWithin_const
added theorem fderivWithin_fun_const
modified theorem fderiv_const
added theorem fderiv_fun_const
modified theorem gradient_const'
modified theorem gradient_const
added theorem gradient_fun_const'
added theorem gradient_fun_const