Structure ModelWithCorners

Modification history

2026-05-16 04:19
MathlibTest/FunPropMinimal.lean
feat(fun_prop): allow fun_prop to call discharger on ModelWithCorners (#39226) …
Added ModelWithCornersView on Github →
2024-10-09 08:43
test/MfldSetTac.lean
chore: adaptations for lean4#5542 (#17564) …
Modified ModelWithCornersView on Github →
2023-12-13 09:43
test/MfldSetTac.lean
chore: rename LocalEquiv to PartialEquiv (#8984) …
Modified ModelWithCornersView on Github →
2023-08-10 19:52
Mathlib/Geometry/Manifold/SmoothManifoldWithCorners.lean
chore: banish `Type _` and `Sort _` (#6499) …
Modified ModelWithCornersView on Github →
2023-06-05 05:02
Mathlib/Geometry/Manifold/SmoothManifoldWithCorners.lean
feat: port Geometry.Manifold.SmoothManifoldWithCorners (#4636)
Added ModelWithCornersView on Github →
2022-09-07 12:54
test/MfldSetTac.lean
feat(Mathlib/Logic/Equiv/LocalEquiv): add the `mfld_set_tac` tactic (#331) …
Added ModelWithCornersView on Github →