Theorem contMDiff_tangentBundleModelSpaceHomeomorph_symm

Modification history

2025-03-06 18:43
Mathlib/Geometry/Manifold/VectorBundle/Tangent.lean
feat: invariance under diffeomorphisms of the Lie bracket of vector fields on manifolds, and Jacobi identity (#22446)
Modified contMDiff_tangentBundleModelSpaceHomeomorph_symmView on Github →
2024-12-09 17:46
Mathlib/Geometry/Manifold/VectorBundle/Tangent.lean
feat: the homeomorphism between the tangent bundle to the model space and the product is a diffeomorphism (#19637)
Added contMDiff_tangentBundleModelSpaceHomeomorph_symmView on Github →