Commit 2025-12-22 21:59 64d91150

View on Github →

refactor: use "@[to_fun]" to generate some lemmas (#32830)

Estimated changes

deleted theorem AnalyticAt.fun_div
added theorem HasDerivAt.neg
added theorem HasDerivAt.sub
deleted theorem HasDerivAtFilter.fun_sub
added theorem HasDerivAtFilter.neg
added theorem HasDerivWithinAt.neg
added theorem HasDerivWithinAt.sub
deleted theorem HasStrictDerivAt.fun_sub
added theorem HasStrictDerivAt.neg
deleted theorem deriv.fun_neg'
deleted theorem deriv.fun_neg
modified theorem deriv.neg
deleted theorem derivWithin.fun_neg
modified theorem derivWithin.neg
deleted theorem HasDerivAt.fun_inv
deleted theorem HasDerivWithinAt.fun_inv
added theorem HasDerivAt.const_smul
deleted theorem HasDerivAt.fun_mul
deleted theorem HasDerivAt.fun_smul
deleted theorem HasDerivWithinAt.fun_mul
deleted theorem HasDerivWithinAt.fun_smul
deleted theorem HasStrictDerivAt.fun_mul
added theorem HasStrictDerivAt.smul
deleted theorem Differentiable.fun_add
deleted theorem Differentiable.fun_neg
deleted theorem Differentiable.fun_sub
deleted theorem DifferentiableAt.fun_add
deleted theorem DifferentiableAt.fun_neg
deleted theorem DifferentiableAt.fun_sub
deleted theorem DifferentiableOn.fun_add
deleted theorem DifferentiableOn.fun_neg
deleted theorem DifferentiableOn.fun_sub
added theorem HasFDerivAt.add
added theorem HasFDerivAt.const_smul
added theorem HasFDerivAt.neg
added theorem HasFDerivAt.sub
deleted theorem HasFDerivAtFilter.fun_add
deleted theorem HasFDerivAtFilter.fun_neg
deleted theorem HasFDerivAtFilter.fun_sub
added theorem HasFDerivWithinAt.add
added theorem HasFDerivWithinAt.neg
added theorem HasFDerivWithinAt.sub
added theorem HasStrictFDerivAt.add
deleted theorem HasStrictFDerivAt.fun_neg
deleted theorem HasStrictFDerivAt.fun_sub
deleted theorem Differentiable.fun_inv
deleted theorem Differentiable.fun_mul
deleted theorem Differentiable.fun_smul
deleted theorem DifferentiableAt.fun_inv
deleted theorem DifferentiableAt.fun_mul
deleted theorem DifferentiableAt.fun_smul
deleted theorem DifferentiableOn.fun_inv
deleted theorem DifferentiableOn.fun_mul
deleted theorem DifferentiableOn.fun_smul
deleted theorem HasFDerivAt.fun_mul'
deleted theorem HasFDerivAt.fun_mul
deleted theorem HasFDerivAt.fun_smul
deleted theorem HasFDerivWithinAt.fun_mul
modified theorem HasFDerivWithinAt.smul
deleted theorem HasStrictFDerivAt.fun_mul
deleted theorem MeromorphicAt.fun_smul
deleted theorem MeromorphicOn.fun_smul
modified theorem MeromorphicOn.smul
deleted theorem CurveIntegrable.fun_neg
deleted theorem CurveIntegrable.fun_zero