Theorem ContMDiff.sum_map

Modification history

2025-02-20 15:30
Mathlib/Geometry/Manifold/ContMDiff/Constructions.lean
chore: rename ContMDiff.sum_{elim,map} (#22131)
Deleted ContMDiff.sum_mapView on Github →
2025-02-17 21:24
Mathlib/Geometry/Manifold/ContMDiff/Constructions.lean
feat: Sum.inl and friends between smooth manifolds are smooth (#20664) …
Added ContMDiff.sum_mapView on Github →