Commit 2020-04-14 11:02 96a07a71

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.