# Commit 2020-08-13 09:22 cc6528e7

View on Github →feat(analysis/calculus/fderiv): multiplication by a complex respects real differentiability (#3731)
If `f`

takes values in a complex vector space and is real-differentiable, then `c f`

is also real-differentiable when `c`

is a complex number. This PR proves this fact and the obvious variations, in the general case of two fields where one is a normed algebra over the other one.
Along the way, some material on `module.restrict_scalars`

is added, notably in a normed space context.