Theorem TangentBundle.continuousLinearMapAt_trivializationAt

Modification history

2025-07-04 16:21
Mathlib/Geometry/Manifold/MFDeriv/Atlas.lean
feat: more API on manifolds (#26501)
Added TangentBundle.continuousLinearMapAt_trivializationAtView on Github →