finite_dimension): add `linear_map.is_open_map_of_finite_dimensional` (#17466)

Commit

3 years ago

feat(topology/algebra/module/finite_dimension): add `linear_map.is_open_map_of_finite_dimensional` (#17466) Also use it to prove `is_open_map_barycentric_coord` without assuming `[finite_dimensional 𝕜 E]`.

Author

urkud

Parents

c005eac4

mathlib c6c8f200 - feat(topology/algebra/module/finite_dimension): add `linear_map.is_open_map_of_finite_dimensional` (#17466)

mathlib
c6c8f200 - feat(topology/algebra/module/finite_dimension): add `linear_map.is_open_map_of_finite_dimensional` (#17466)