Commit 2024-11-25 09:33 a5ae0c1c

chore: remove the Smooth alias for infinitely differentiable functions between manifolds (#19296) The abbreviation Smooth for ContMDiff with infinite smoothness had been introduced in mathlib in ancient times. This has lead to a big API duplication, for no visible gain. We deprecate this abbreviation (with its friends SmoothAt and so on) and all the lemmas involving it. In the longer run, we might consider reintroducing it as a mere notation (without any specific API), but this is not part of this PR, devoted purely to the deprecation. No mathematical content added.