mathlib3

39db98c8 - feat(analysis/normed_space/add_torsor_bases): the convex hull has non-empty interior iff the affine span is top (#9727)

feat(analysis/normed_space/add_torsor_bases): the convex hull has non-empty interior iff the affine span is top (#9727) Formalized as part of the Sphere Eversion project. Co-authored-by: Patrick Massot <patrickmassot@free.fr>