Def Pretrivialization.continuousLinearMap

Modification history

2023-07-06 15:47

Mathlib/Topology/VectorBundle/Hom.lean

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

Added Pretrivialization.continuousLinearMap View on Github →