Mathlib v3 is deprecated. Go to Mathlib v4

Structure 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) …
Deleted cont_mdiff_mapView on Github →
2022-02-23 00:45
src/geometry/manifold/cont_mdiff_map.lean
chore(analysis): rename times_cont_diff (#12227) …
Added cont_mdiff_mapView on Github →