Def tangentBundleModelSpaceDiffeomorph

Modification history

2024-12-09 17:46

Mathlib/Geometry/Manifold/MFDeriv/Tangent.lean

feat: the homeomorphism between the tangent bundle to the model space and the product is a diffeomorphism (#19637)

Added tangentBundleModelSpaceDiffeomorph View on Github →