Commit 2026-07-11 11:20 5e1cacba
View on Github →feat: a map is smooth iff its post-composition with an immersion is (#28865)
A future PR will use this to golf the results in Icc/Instances.lean; we will also use this to study bordism theory.
feat: a map is smooth iff its post-composition with an immersion is (#28865)
A future PR will use this to golf the results in Icc/Instances.lean; we will also use this to study bordism theory.