Theorem IsLocalDiffeomorphAt.mfderivToContinuousLinearEquiv_coe

Modification history

2025-05-08 20:56
Mathlib/Geometry/Manifold/LocalDiffeomorph.lean
feat: differential of a local diffeomorphism is a continuous linear equivalence (#8738) …
Added IsLocalDiffeomorphAt.mfderivToContinuousLinearEquiv_coeView on Github →