mathlib
96a07a71 - refactor(analysis/calculus/deriv): split comp and scomp (#2410)

Commit
5 years ago
refactor(analysis/calculus/deriv): split comp and scomp (#2410) The derivative of the composition of a function and a scalar function was written using `smul`, regardless of the fact that the first function was vector-valued (in which case `smul` is not avoidable) or scalar-valued (in which case it can be replaced by `mul`). Instead, this PR introduces two sets of lemmas (named `scomp` for the first type and `comp` for the second type) to get the usual multiplication in the formula for the derivative of the composition of two scalar functions.
Author
Parents
Loading