Mathlib v3 is deprecated. Go to Mathlib v4

Theorem continuous_linear_equiv.mfderiv_within_eq

Modification history

2021-03-26 14:24

src/geometry/manifold/mfderiv.lean

feat(geometry/manifold/mfderiv): differentiability of `f : E ≃L[𝕜] E'` (#6850)

Added continuous_linear_equiv.mfderiv_within_eq View on Github →