mathlib

cc6528e7 - feat(analysis/calculus/fderiv): multiplication by a complex respects real differentiability (#3731)

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.