Mathlib v3 is deprecated. Go to Mathlib v4

Def continuous_linear_map.in_coordinates

Modification history

2023-04-25 17:43
src/topology/vector_bundle/basic.lean
feat(topology/vector_bundle/basic): define in_coordinates (#18826) …
Added continuous_linear_map.in_coordinatesView on Github →