Mathlib Changelog
v4
Changelog
About
Github
Def
ModelWithCorners.of_convex_range
Modification history
2025-12-20 08:12
Mathlib/Geometry/Manifold/IsManifold/Basic.lean
fix: rename definitions which use underscores in their name (#33103) …
Deleted
ModelWithCorners.of_convex_range
View on Github →
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.of_convex_range
View on Github →