Def Manifold.Elab.Elab.findModel

Modification history

2026-02-23 10:04
Mathlib/Geometry/Manifold/Notation.lean
feat: support products and disjoint unions in the differential geometry elaborators (#30463) …
Deleted Manifold.Elab.Elab.findModelView on Github →
2025-10-08 14:28
Mathlib/Geometry/Manifold/Notation.lean
feat: custom elaborators for differential geometry (#27021) …
Added Manifold.Elab.Elab.findModelView on Github →