Commit 2022-04-06 15:26 06bdd8bc

View on Github →

feat(geometry/manifold/tangent_bundle): adapt the definition to the new vector bundle definition (#13199) Also a few tweaks to simplify the defeq behavior of tangent spaces.

Estimated changes

Modified src/geometry/manifold/cont_mdiff.lean

added def tangent_bundle.zero_section

Modified src/geometry/manifold/tangent_bundle.lean

added theorem basic_smooth_vector_bundle_core.coord_change_continuous

added theorem basic_smooth_vector_bundle_core.coord_change_smooth

modified def tangent_bundle.proj

modified def tangent_bundle

modified def tangent_space