mathlib

c950c45e - feat(analysis/calculus/[f]deriv): derivative of pointwise composition/application of continuous linear maps (#9174)

feat(analysis/calculus/[f]deriv): derivative of pointwise composition/application of continuous linear maps (#9174) This introduces useful analogs to the product rule when working with derivatives in spaces of continuous linear maps.