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,AlgebraicGeometry): remove mathlib3 names in doc comments #11955
Conversation
Mostly automatic, with a few manual corrections.
@@ -298,7 +298,7 @@ instance instLinearOrderedCommMonoidWithZeroMultiplicativeOrderDual | |||
{ Multiplicative.orderedCommMonoid, Multiplicative.linearOrder with | |||
zero := Multiplicative.ofAdd (⊤ : α) | |||
zero_mul := @top_add _ (_) | |||
-- Porting note: Here and elsewhere in the file, just `zero_mul` worked in Lean 3. See | |||
-- Porting note: Here and elsewhere in the file, just `MulZeroClass.zero_mul` worked in Lean 3. See |
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.
Should this one be reverted?
2684e34
to
205d775
Compare
Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Thanks for the careful review. I have addressed all comments. |
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 Ruben-VandeVelde. |
bors merge |
bors r- |
bors d+ |
✌️ grunweg can now approve this pull request. To approve and merge a pull request, simply reply with |
…#11955) Mostly automatic, with a few manual corrections.
Canceled. |
Please merge after CI is complete. Thanks! |
Thanks for the review. |
…#11955) Mostly automatic, with a few manual corrections.
Pull request successfully merged into master. Build succeeded: |
…#11955) Mostly automatic, with a few manual corrections.
…#11955) Mostly automatic, with a few manual corrections.
…#11955) Mostly automatic, with a few manual corrections.
…#11955) Mostly automatic, with a few manual corrections.
Mostly automatic, with a few manual corrections.