[Merged by Bors] - feat(Geometry/Convex): modules are convex spaces#39531

YaelDillies wants to merge 4 commits into

leanprover-community:masterleanprover-community/mathlib4:masterfrom

YaelDillies:convex_space_moduleYaelDillies/mathlib4:convex_space_moduleCopy head branch name to clipboard