Theorem ContMDiff.iff_comp_isImmersion

Modification history

2026-07-11 11:20
Mathlib/Geometry/Manifold/Immersion.lean
feat: a map is smooth iff its post-composition with an immersion is (#28865) …
Added ContMDiff.iff_comp_isImmersionView on Github →