mathlib

268073ae - feat(geometry/manifold): derivative of the zero section of the tangent bundle (#4292)

feat(geometry/manifold): derivative of the zero section of the tangent bundle (#4292) We show that the zero section of the tangent bundle to a smooth manifold is smooth, and compute its derivative. Along the way, some streamlining of supporting material.