Def Manifold.Elab.Elab.findModelInner

Modification history

2026-06-23 08:28
Mathlib/Geometry/Manifold/Notation.lean
feat: properly support inferring a model with corners on a `Bundle.TotalSpace` (#40047) …
Deleted Manifold.Elab.Elab.findModelInnerView on Github →
2026-02-23 10:04
Mathlib/Geometry/Manifold/Notation.lean
feat: support products and disjoint unions in the differential geometry elaborators (#30463) …
Added Manifold.Elab.Elab.findModelInnerView on Github →