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] - feat (Mathlib.RingTheory.Ideal.Operations) : Change hypotheses from ring to semiring #8469
Conversation
There was indeed a mistake in the CI: #8471. Merged master, which should fix it. |
Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>
Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
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.
Some comments on spaces. Otherwise LGTM.
Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>
Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>
✌️ XavierXarles can now approve this pull request. To approve and merge a pull request, simply reply with |
Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com>
Can you please address my other comments as well? |
Changed docs of map_of_equiv and comap_of_equiv as requested.
I hope I did all requested changes. The name map_comap_of_equiv (and all the others) are not mine, so I didn't changed, not to affect other parts of mathlib. |
Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
Yes, I had mixed feelings when asking you to fix something that was already wrong before, but thanks for fixing it! bors merge |
…ing to semiring (#8469) Moved some results from ring to semiring. Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com> Co-authored-by: Xavier Xarles <56635243+XavierXarles@users.noreply.github.com>
Pull request successfully merged into master. Build succeeded: |
…ing to semiring (#8469) Moved some results from ring to semiring. Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com> Co-authored-by: Xavier Xarles <56635243+XavierXarles@users.noreply.github.com>
Moved some results from ring to semiring.
In Mathlib.RingTheory.Ideal.Operations I moved two results from ring to semiring with the same proof, and two I changed the proof.