Mathlib v3 is deprecated. Go to Mathlib v4

Theorem smooth_at_hom_bundle

Modification history

2023-05-17 16:46

src/geometry/manifold/vector_bundle/hom.lean

feat(geometry/manifold/vector_bundle/hom): the hom bundle is smooth (#18828) …

Added smooth_at_hom_bundle View on Github →