Commit 2024-10-11 06:22 1cc075db

feat: remove the SmoothManifoldWithCorners assumption in the definition of tangent spaces (#17616) Currently, the definition of the tangent space to a manifold includes (as a nolinted unused parameter) the assumption that the manifold is smooth. However, many statements make sense without this assumption (notably differentiability statements), and including it forces to include a lot of machinery on smooth bundles in the definition of MDifferentiableWithinAt, say. We remove the assumption from the definition. This makes it possible to remove the assumption SmoothManifoldWithCorners from a bunch of statements (including some where it is clearly irrelevant), and disentangle our import structure, without any bad consequence as far as I can tell. There is nothing added or removed in this PR, just moving things around and removing [SmoothManifoldWithCorners I M] assumptions.