mathlib3

5c3cdd21 - feat(analysis/normed_space/add_torsor_bases): barycentric coordinates are open maps (in finite dimensions over a complete field) (#9543)

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.