Mathlib v3 is deprecated. Go to Mathlib v4

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.

Estimated changes