Commit 2025-02-17 21:24 f7c4a817

feat: Sum.inl and friends between smooth manifolds are smooth (#20664) We prove that the following maps between manifolds are smooth:

• Sum.inl, Sum.inr, as well as Sum.map_elim and Sum.swap
• Furthermore, Sum.map_elim is C^n iff both components are. Since the file we're editing now contains material both about products and disjoint unions, we rename the file to Constructions. From my bordism theory project.