Theorem Diffeomorph.mfderivToContinuousLinearEquiv_coe

Modification history

2025-12-22 11:55
Mathlib/Geometry/Manifold/LocalDiffeomorph.lean
refactor(Analysis,Geometry): assume `n ≠ 0`, not `1 ≤ n` (#33131) …
Modified Diffeomorph.mfderivToContinuousLinearEquiv_coeView on Github →
2025-05-08 20:56
Mathlib/Geometry/Manifold/LocalDiffeomorph.lean
feat: differential of a local diffeomorphism is a continuous linear equivalence (#8738) …
Added Diffeomorph.mfderivToContinuousLinearEquiv_coeView on Github →