Theorem UniqueMDiffOn.tangentBundle_proj_preimage
Modification history
2024-10-11 06:22
Mathlib/Geometry/Manifold/MFDeriv/Tangent.lean
feat: remove the `SmoothManifoldWithCorners` assumption in the definition of tangent spaces (#17616) …
Modified UniqueMDiffOn.tangentBundle_proj_preimageView on Github →