Commit 2023-02-24 15:00 5be98b95

feat(geometry/manifold/vector_bundle): smooth_fiberwise_linear groupoid (#17302) Let B be a smooth manifold and F a normed space. We build the groupoid of local homeomorphisms of B × F which are "smooth and fibrewise linear": that is, they are of the form λ x, (x.1, φ x.1 x.2) for some function φ from B to the automorphisms of F, which is smooth and has smooth inverse on the proposed domain. Membership in this groupoid is the natural property characterizing the transition functions of a smooth vector bundle over B modelled on F.