Def smoothFiberwiseLinear

Modification history

2023-06-24 05:35

Mathlib/Geometry/Manifold/VectorBundle/FiberwiseLinear.lean

feat: port Geometry.Manifold.VectorBundle.FiberwiseLinear (#5440)

Added smoothFiberwiseLinear View on Github →