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: port Order.RelIso.Group #813
Conversation
Signed-off-by: thirdsgames <thirdsgames2018@gmail.com>
Signed-off-by: thirdsgames <thirdsgames2018@gmail.com>
Signed-off-by: thirdsgames <thirdsgames2018@gmail.com>
The convention I have already used was to use |
Some other PRs agreed with your convention however. I think we'll stick to your convention. |
bors merge |
mathlib3 SHA: 62a5626868683c104774de8d85b9855234ac807c I would appreciate advice on naming lemmas about coercions, the porting guide doesn't say what to do.
Pull request successfully merged into master. Build succeeded:
|
Regenerated from the [port status wiki page](https://github.com/leanprover-community/mathlib/wiki/mathlib4-port-status). Relates to the following PRs: * `algebra.order.sub.canonical`: leanprover-community/mathlib4#814 * `category_theory.category.Rel`: leanprover-community/mathlib4#822 * `category_theory.category.basic`: leanprover-community/mathlib4#749 * `category_theory.functor.basic`: leanprover-community/mathlib4#749 * `category_theory.functor.category`: leanprover-community/mathlib4#749 * `category_theory.functor.functorial`: leanprover-community/mathlib4#822 * `category_theory.isomorphism`: leanprover-community/mathlib4#749 * `category_theory.natural_transformation`: leanprover-community/mathlib4#749 * `category_theory.thin`: leanprover-community/mathlib4#822 * `combinatorics.quiver.basic`: leanprover-community/mathlib4#749 * `combinatorics.quiver.path`: leanprover-community/mathlib4#811 * `data.psigma.order`: leanprover-community/mathlib4#815 * `data.stream.defs`: leanprover-community/mathlib4#665 * `order.boolean_algebra`: leanprover-community/mathlib4#794 * `order.heyting.basic`: leanprover-community/mathlib4#793 * `order.rel_iso.group`: leanprover-community/mathlib4#813
Regenerated from the [port status wiki page](https://github.com/leanprover-community/mathlib/wiki/mathlib4-port-status). Relates to the following PRs: * `algebra.order.sub.canonical`: leanprover-community/mathlib4#814 * `category_theory.category.Rel`: leanprover-community/mathlib4#822 * `category_theory.category.basic`: leanprover-community/mathlib4#749 * `category_theory.functor.basic`: leanprover-community/mathlib4#749 * `category_theory.functor.category`: leanprover-community/mathlib4#749 * `category_theory.functor.functorial`: leanprover-community/mathlib4#822 * `category_theory.isomorphism`: leanprover-community/mathlib4#749 * `category_theory.natural_transformation`: leanprover-community/mathlib4#749 * `category_theory.thin`: leanprover-community/mathlib4#822 * `combinatorics.quiver.basic`: leanprover-community/mathlib4#749 * `combinatorics.quiver.path`: leanprover-community/mathlib4#811 * `data.psigma.order`: leanprover-community/mathlib4#815 * `data.stream.defs`: leanprover-community/mathlib4#665 * `order.boolean_algebra`: leanprover-community/mathlib4#794 * `order.heyting.basic`: leanprover-community/mathlib4#793 * `order.rel_iso.group`: leanprover-community/mathlib4#813
mathlib3 SHA: 62a5626868683c104774de8d85b9855234ac807c
I would appreciate advice on naming lemmas about coercions, the porting guide doesn't say what to do.