Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Commit
2021-03-26 14:24
f0bfb25c
View on Github →
feat(geometry/manifold/mfderiv): differentiability of
f : E ≃L[𝕜] E'
(
#6850
)
Estimated changes
Modified
src/geometry/manifold/mfderiv.lean
added
theorem
continuous_linear_equiv.mfderiv_eq
added
theorem
continuous_linear_equiv.mfderiv_within_eq