Def Trivialization.continuousLinearMap

Modification history

2023-07-06 15:47

Mathlib/Topology/VectorBundle/Hom.lean

feat: port Topology.VectorBundle.Hom (#4514)

Added Trivialization.continuousLinearMap View on Github →