Theorem Bundle.Trivial.trivialization_target

Modification history

2025-06-19 12:16

Mathlib/Topology/FiberBundle/Constructions.lean

feat: more uses of `simps` in fiber bundles and vector bundles (#26121)

Deleted Bundle.Trivial.trivialization_target View on Github →

2023-05-18 07:49

Mathlib/Topology/FiberBundle/Constructions.lean

feat: port Topology.FiberBundle.Constructions (#3145)

Added Bundle.Trivial.trivialization_target View on Github →