-
Notifications
You must be signed in to change notification settings - Fork 251
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - doc(Algebra/Ring): add docstring for CommRing
and CommSemiring
#11894
Conversation
This PR resolves some nolints by adding docstrings for `CommRing` and `CommSemiring`.
CommRing
and CommSemiring
CommRing
and CommSemiring
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Done @eric-wieser |
These docstrings existed in Lean 3. Can you see what they were? |
Do you mean these? @YaelDillies |
Yep! |
Ok, should I copy-paste them here with the obvious minor adjustments or those committed in this PR are fine? |
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
Done @YaelDillies |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thanks!
maintainer merge
🚀 Pull request has been placed on the maintainer queue by YaelDillies. |
Please merge when CI clears. Thanks. bors delegate+ |
✌️ pitmonticone can now approve this pull request. To approve and merge a pull request, simply reply with |
bors merge |
…11894) This PR resolves some nolints by adding docstrings for `CommRing` and `CommSemiring`.
🚀 Pull request has been placed on the maintainer queue by YaelDillies. |
bors merge |
Already running a review |
Pull request successfully merged into master. Build succeeded: |
CommRing
and CommSemiring
CommRing
and CommSemiring
…11894) This PR resolves some nolints by adding docstrings for `CommRing` and `CommSemiring`.
…11894) This PR resolves some nolints by adding docstrings for `CommRing` and `CommSemiring`.
…11894) This PR resolves some nolints by adding docstrings for `CommRing` and `CommSemiring`.
…11894) This PR resolves some nolints by adding docstrings for `CommRing` and `CommSemiring`.
…11894) This PR resolves some nolints by adding docstrings for `CommRing` and `CommSemiring`.
This PR resolves some nolints by adding docstrings for
CommRing
andCommSemiring
.