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.