Commit 2023-05-22 18:33 314e4d60

View on Github →

feat: port Topology.VectorBundle.Constructions (#4207)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/VectorBundle/Constructions.lean

added theorem Bundle.Trivial.trivialization.coordChangeL

added theorem Trivialization.continuousLinearEquivAt_prod

added theorem Trivialization.coordChangeL_prod

added theorem Trivialization.prod_apply