Structure Manifold.Elab.Elab.NormedSpaceInfo

Modification history

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.NormedSpaceInfoView on Github →