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

Commit

4 years ago

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

Author

urkud

urkud

Parents

Loading