mathlib

5be98b95 - feat(geometry/manifold/vector_bundle): `smooth_fiberwise_linear` groupoid (#17302)

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`. Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com> Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com>