Commit 2021-10-06 18:27 5c3cdd21

feat(analysis/normed_space/add_torsor_bases): barycentric coordinates are open maps (in finite dimensions over a complete field) (#9543) Using the open mapping theorem with a one-dimensional codomain feels a bit ridiculous but I see no reason not to do so. Formalized as part of the Sphere Eversion project.