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(order/hom): rearrange definitions of order_{hom,iso,embedding}
#10752
Conversation
* rename `order/order_hom.lean` to `order/hom/basic.lean` * move `order_hom.complete_lattice` to a new file `order/hom/lattice.lean` * reduce imports
8a48c34
to
15ef754
Compare
🎉 Great news! Looks like all the dependencies have been resolved: 💡 To add or remove a dependency please update this issue/PR description. Brought to you by Dependent Issues (:robot: ). Happy coding! |
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 🎉
If CI passes, please remove the label awaiting-CI
and merge this yourself, by adding a comment bors r+
.
bors d+
✌️ Vierkantor can now approve this pull request. To approve and merge a pull request, simply reply with |
bors merge |
#10752) We symmetrize the locations of `rel_{hom,iso,embedding}` and `order_{hom,iso,embedding}` by putting the `rel_` definitions in `order/rel_iso.lean` and the `order_` definitions in `order/hom/basic.lean`. (`order_hom.lean` needed to be split up to fix an import loop.) Requested by @YaelDillies. ## Moved definitions * `order_hom`, `order_iso`, `order_embedding` are now in `order/hom/basic.lean` * `order_hom.has_sup` ... `order_hom.complete_lattice` are now in `order/hom/lattice.lean` ## Other changes Some import cleanup.
Pull request successfully merged into master. Build succeeded: |
order_{hom,iso,embedding}
order_{hom,iso,embedding}
We symmetrize the locations of
rel_{hom,iso,embedding}
andorder_{hom,iso,embedding}
by putting therel_
definitions inorder/rel_iso.lean
and theorder_
definitions inorder/hom/basic.lean
. (order_hom.lean
needed to be split up to fix an import loop.) Requested by @YaelDillies.Moved definitions
order_hom
,order_iso
,order_embedding
are now inorder/hom/basic.lean
order_hom.has_sup
...order_hom.complete_lattice
are now inorder/hom/lattice.lean
Other changes
Some import cleanup.
preorder_hom
toorder_hom
#10750