-
Notifications
You must be signed in to change notification settings - Fork 298
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] - chore(logic/embedding): move some algebra content #7776
Conversation
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.
This looks like a reasonable home to me.
bors r+
This moves a lemma about multiplication by an element in a left/right cancellative semigroup being an embedding out of `logic.embedding`. I didn't find a great home for it, but put it with some content about regular elements, which is at least talking about similar mathematics. This removes the only direct import from the `logic/` directory to the `algebra/` directory. There are still indirect imports from `logic.small`, which currently brings in `fintype` and hence the whole algebra hierarchy. I'll look at that separately.
bors r- Just in case CI fails |
✌️ semorrison can now approve this pull request. To approve and merge a pull request, simply reply with |
Canceled. |
bors merge |
This moves a lemma about multiplication by an element in a left/right cancellative semigroup being an embedding out of `logic.embedding`. I didn't find a great home for it, but put it with some content about regular elements, which is at least talking about similar mathematics. This removes the only direct import from the `logic/` directory to the `algebra/` directory. There are still indirect imports from `logic.small`, which currently brings in `fintype` and hence the whole algebra hierarchy. I'll look at that separately.
Pull request successfully merged into master. Build succeeded: |
This moves a lemma about multiplication by an element in a left/right cancellative semigroup being an embedding out of
logic.embedding
. I didn't find a great home for it, but put it with some content about regular elements, which is at least talking about similar mathematics.This removes the only direct import from the
logic/
directory to thealgebra/
directory. There are still indirect imports fromlogic.small
, which currently brings infintype
and hence the whole algebra hierarchy. I'll look at that separately.