Commit 2024-02-06 18:38 62b46d13

View on Github →

feat: define ContinuousMultilinearMap.linearDeriv and show it's the fderiv (#9846)

Estimated changes

Modified Mathlib/Analysis/Analytic/Basic.lean

Modified Mathlib/Analysis/Analytic/CPolynomial.lean

added theorem HasFiniteFPowerSeriesOnBall.mk'

Modified Mathlib/Analysis/Calculus/FDeriv/Analytic.lean

added theorem ContinuousMultilinearMap.cPolynomialAt

added theorem ContinuousMultilinearMap.cPolyomialOn

added theorem ContinuousMultilinearMap.changeOriginSeries_support

added theorem ContinuousMultilinearMap.changeOrigin_toFormalMultilinearSeries

added theorem ContinuousMultilinearMap.contDiff

added theorem ContinuousMultilinearMap.contDiffAt

Modified Mathlib/Analysis/Calculus/FormalMultilinearSeries.lean

Modified Mathlib/Topology/Algebra/Module/Multilinear/Basic.lean

added def ContinuousMultilinearMap.linearDeriv

added theorem ContinuousMultilinearMap.linearDeriv_apply