Mathlib Changelog
v4
Changelog
About
Github
Theorem
ContinuousLinearMap.hasStrictFDerivAt_of_bilinear
Modification history
2024-04-05 06:15
Mathlib/Analysis/Calculus/FDeriv/Bilinear.lean
feat: `deriv` versions of composition lemmas with bilinear maps (#11868) …
Added
ContinuousLinearMap.hasStrictFDerivAt_of_bilinear
View on Github →