Theorem ModelWithCorners.range_eq_univ_of_not_isRCLikeNormedField

Modification history

2025-06-30 10:32
Mathlib/Geometry/Manifold/IsManifold/Basic.lean
feat: require that the range of a real or complex model with corners is convex (#25824) …
Added ModelWithCorners.range_eq_univ_of_not_isRCLikeNormedFieldView on Github →