Mathlib Changelog
v4
Changelog
About
Github
Theorem
interior_euclideanQuadrant
Modification history
2025-06-30 10:32
Mathlib/Geometry/Manifold/Instances/Real.lean
feat: require that the range of a real or complex model with corners is convex (#25824) …
Added
interior_euclideanQuadrant
View on Github →