Commit 2025-10-23 10:55 8acb4f34

feat: local frames in a vector bundle (#30338) We define a predicate IsLocalFrameOn, for a collection of sections of a vector bundle to be a local frame. We provide some basic API, such as the coefficients of a section t w.r.t. a local frame, or proving smoothness of t via proving the smoothness of its local frame coefficients. A future PR will construct actual local frames, and use these to define the local extension of a tangent vector to a vector field near a point. From the path towards geodesics and the Levi-Civita connection.