Mathlib v3 is deprecated. Go to Mathlib v4

Def cont_mdiff_map

Modification history

2023-06-20 04:52
src/geometry/manifold/cont_mdiff_map.lean
refactor(geometry/manifold/cont_mdiff_map): redefine as subtype not structure (#19147) …
Added cont_mdiff_mapView on Github →