[Merged by Bors] - chore: remove the Smooth alias for infinitely differentiable functions between manifolds#19296
[Merged by Bors] - chore: remove the Smooth alias for infinitely differentiable functions between manifolds#19296
Smooth alias for infinitely differentiable functions between manifolds#19296Conversation
PR summary 06eb2911c8Import changes for modified filesNo significant changes to the import graph Import changes for all files
|
grunweg
left a comment
There was a problem hiding this comment.
I've reviewed the changes to the MFDeriv, Sheaf and VectorBundle directories: only very minor questions so far. Two larger points worth flagging:
- would you like to remove the now-used
abbrevsSmoothetc? - the deprecation dates in your lemmas are slightly inconsistent: not a big deal, in any case
| theorem smoothOn_coordChangeL : | ||
| SmoothOn IB 𝓘(𝕜, F →L[𝕜] F) (fun b : B => (e.coordChangeL 𝕜 e' b : F →L[𝕜] F)) | ||
| theorem contMDiffOn_coordChangeL : | ||
| ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun b : B => (e.coordChangeL 𝕜 e' b : F →L[𝕜] F)) |
There was a problem hiding this comment.
Do you mean \top instead of n?
There was a problem hiding this comment.
The version with a general n is stronger than the version with top (well, they are equivalent, but often the version with a general implicit n is more convenient, for instance when chaining).
| theorem smoothOn_symm_coordChangeL : | ||
| SmoothOn IB 𝓘(𝕜, F →L[𝕜] F) (fun b : B => ((e.coordChangeL 𝕜 e' b).symm : F →L[𝕜] F)) | ||
| theorem contMDiffOn_symm_coordChangeL : | ||
| ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun b : B => ((e.coordChangeL 𝕜 e' b).symm : F →L[𝕜] F)) |
Not sure if it's a question on the current version of the PR. In the current version of the PR,
Yes, it depends on the day I've made the change. Since it's just by one or two days, I wouldn't mind. Maybe one day CI will automagically change the deprecated dates to the date the PR is merged in master, but we're not there yet :-) |
|
I looked through the changes. The deduplication of API is worth the occasional addition of |
…ons 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.
|
Pull request successfully merged into master. Build succeeded: |
Smooth alias for infinitely differentiable functions between manifoldsSmooth alias for infinitely differentiable functions between manifolds
The abbreviation
SmoothforContMDiffwith 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 friendsSmoothAtand 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.