[Merged by Bors] - chore: ensure inherit_doc-ed notation is mentioned in the underlying doc-string#20684
[Merged by Bors] - chore: ensure inherit_doc-ed notation is mentioned in the underlying doc-string#20684
inherit_doc-ed notation is mentioned in the underlying doc-string#20684Conversation
…is notation This is not exhaustive, but covers everything up to (excluding) Mathlib/Algebra/Star.
PR summary b76c60e824Import changes for modified filesNo significant changes to the import graph Import changes for all files
Declarations diffNo declarations were harmed in the making of this PR! 🐙 You can run this locally as follows## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>
## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>The doc-module for Decrease in tech debt: (relative, absolute) = (17.00, 0.03)
Current commit b76c60e824 You can run this locally as
|
|
@j-loreaux This performs some of the menial task you asked me to on #11905. Would you like to review (part of) this PR? |
| /-- Composing two partial equivs, by restricting to the maximal domain where their composition | ||
| is well defined. -/ | ||
| is well defined. | ||
| Within the `Manifold` namespace, there is the notation `e ≫ f` for this. |
There was a problem hiding this comment.
This one seems strange on its face. Can you double check?
There was a problem hiding this comment.
This notation is defined in Geometry/Manifold/ChartedSpace.lean. I'm not sure if this is the best solution; I could also simply add a comment there.
| /-- Composing two partial homeomorphisms, by restricting to the maximal domain where their | ||
| composition is well defined. -/ | ||
| composition is well defined. | ||
| Within the `Manifold` namespace, there is the notation `e ≫ₕ f` for this. -/ |
There was a problem hiding this comment.
For my laziness, can you point me to where this is
There was a problem hiding this comment.
Similarly: in Geometry/Manifold/ChartedSpace.lean
Co-authored-by: Matthew Robert Ballard <100034030+mattrobball@users.noreply.github.com>
Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
mattrobball
left a comment
There was a problem hiding this comment.
Looks to good to me.
Two larger points for the future:
- a
@[scoped NS]attribute might be appealing cosmetically - rarely do I read a math paper that says "Notation is...". It is almost always "denoted as ..."
|
bors delegate+ |
|
✌️ grunweg can now approve this pull request. To approve and merge a pull request, simply reply with |
|
Thanks for the review! I have audited all occurrences (on a long train ride); this should be good to go now. |
|
As this PR is labelled bors merge |
…g doc-string (#20684) This is not exhaustive. Add some `inherit_doc` when appropriate. Co-authored-by: grunweg <rothgami@math.hu-berlin.de>
|
Pull request successfully merged into master. Build succeeded: |
inherit_doc-ed notation is mentioned in the underlying doc-stringinherit_doc-ed notation is mentioned in the underlying doc-string
This is not exhaustive. Add some
inherit_docwhen appropriate.Commits can be reviewed separately.