Commit 2025-06-25 15:59 2545ec6d

View on Github →

chore: add fun_ versions in the files on one-dimensional derivatives (#26355) Also dispatch fun_prop attributes from the dedicated file to the right places in the library.

Estimated changes

added theorem HasDerivAt.fun_sum
added theorem deriv.fun_neg'
added theorem deriv.fun_neg
modified theorem deriv.neg'
modified theorem deriv.neg
added theorem derivWithin.fun_neg
modified theorem derivWithin.neg
added theorem derivWithin_fun_add
added theorem derivWithin_fun_sub
added theorem derivWithin_fun_sum
modified theorem deriv_add_const'
modified theorem deriv_add_const
modified theorem deriv_const_sub
added theorem deriv_fun_add
added theorem deriv_fun_sub
added theorem deriv_fun_sum
modified theorem deriv_neg''
modified theorem deriv_neg'
modified theorem deriv_sub_const
modified theorem hasDerivAt_neg'
added theorem Differentiable.fun_div
added theorem HasDerivAt.fun_div
added theorem HasDerivAt.fun_inv
added theorem derivWithin_fun_div
added theorem derivWithin_fun_inv'
added theorem deriv_fun_div
added theorem deriv_fun_inv''
added theorem HasDerivAt.fun_mul
added theorem HasDerivAt.fun_smul
modified theorem derivWithin_finset_prod
added theorem derivWithin_fun_mul
added theorem derivWithin_fun_smul
modified theorem deriv_const_smul'
added theorem deriv_fun_const_smul'
added theorem deriv_fun_const_smul
added theorem deriv_fun_finset_prod
added theorem deriv_fun_mul
added theorem deriv_fun_smul
added theorem HasDerivAt.fun_pow
added theorem derivWithin_fun_pow'
added theorem deriv_fun_pow''
deleted theorem differentiableAt_id'
added theorem differentiable_fun_id
deleted theorem differentiable_id'
added theorem Differentiable.fun_inv
added theorem Differentiable.fun_mul
added theorem Differentiable.fun_pow
modified theorem Differentiable.pow
added theorem HasFDerivAt.fun_mul'
added theorem HasFDerivAt.fun_mul
added theorem HasFDerivAt.fun_smul
added theorem fderivWithin_fun_mul'
added theorem fderivWithin_fun_mul
added theorem fderivWithin_fun_smul
added theorem fderiv_fun_mul'
added theorem fderiv_fun_mul
added theorem fderiv_fun_smul
deleted theorem iteratedDerivWithin_neg'
added theorem iteratedDeriv_fun_neg