Def IsLocalDiffeomorphAt.mfderivToContinuousLinearEquiv

Modification history

2026-04-17 14:24
Mathlib/Geometry/Manifold/LocalDiffeomorph.lean
chore(Geometry/Manifold): don't expose definitions depending on choice (#37358) …
Added IsLocalDiffeomorphAt.mfderivToContinuousLinearEquivView on Github →