Commit 2025-07-18 08:44 88b155d9

feat: fderiv lemmas for pow (#24351) This generalizes the lemmas about fderiv fun x => f x ^ n to work over arbitrary normed modules and (noncommutative) algebras. Following the convention set by the lemmas about fderiv and *, we use 'd names for the non-commutative variants. The naming is still a little confusing around derivatives (see #mathlib4 > deriv neg lemmas @ 💬), but having these results with some names is better than not having them at all. Moves:

• deriv_fun_pow'' -> deriv_fun_pow
• deriv_pow'' -> deriv_pow
• deriv_pow -> deriv_pow_field
• derivWithin_pow' -> derivWithin_pow_field Deletions:
• deriv_pow'