Mathlib v3 is deprecated. Go to Mathlib v4

Theorem continuous_linear_map.in_coordinates_eq

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_coordinates_eqView on Github →