Theorem contMDiff_of_contMDiff_inl

Modification history

2025-02-17 21:24
Mathlib/Geometry/Manifold/ContMDiff/Constructions.lean
feat: Sum.inl and friends between smooth manifolds are smooth (#20664) …
Added contMDiff_of_contMDiff_inlView on Github →