Commit 2025-06-30 10:32 b26977ff

feat: require that the range of a real or complex model with corners is convex (#25824) This is important to ensure that the distance coming from a Riemannian metric generates the same topology as the original one. See Zulip discussion at #mathlib4 > Fixing the definition of models with corners @ 💬