Commit 2022-11-11 10:11 c6c8f200
View on Github →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].