-
Notifications
You must be signed in to change notification settings - Fork 259
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 Algebra.Order.WithZero #903
Conversation
Do you think that repetitive instance names like |
Good question. I think there was a linter in Lean 3 which prevented this kind of thing, or maybe the instance auto-naming convention was better? Feel free to do as you think best or to start a Zulip conversation. |
I merged the renaming of these instances about |
bors merge |
mathlib3 655994e298904d7e5bbd1e18c95defd7b543eb94 ~~All remaining issues are elaboration problems involving the order-dual. I think these should be debugged carefully, but I am not sure whether I will have time this weekend, so help is welcome.~~ I fixed these with a bunch of `@` and opened a [Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Type.20synonyms). - [x] depends on #910 - [x] depends on #923 Co-authored-by: Jon <jon.eugster@gmx.ch> Co-authored-by: Jon Eugster <eugster.jon@gmail.com> Co-authored-by: Jon Eugster <Jon.Eugster@hhu.de>
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.euclidean_domain.basic`: leanprover-community/mathlib4#919 * `algebra.field.basic`: leanprover-community/mathlib4#975 * `algebra.group.opposite`: leanprover-community/mathlib4#912 * `algebra.group.prod`: leanprover-community/mathlib4#968 * `algebra.group.with_one.units`: leanprover-community/mathlib4#955 * `algebra.group_power.ring`: leanprover-community/mathlib4#979 * `algebra.hom.equiv.type_tags`: leanprover-community/mathlib4#943 * `algebra.hom.ring`: leanprover-community/mathlib4#958 * `algebra.invertible`: leanprover-community/mathlib4#930 * `algebra.order.field.canonical.basic`: leanprover-community/mathlib4#1018 * `algebra.order.field.canonical.defs`: leanprover-community/mathlib4#985 * `algebra.order.field.inj_surj`: leanprover-community/mathlib4#1017 * `algebra.order.group.densely_ordered`: leanprover-community/mathlib4#956 * `algebra.order.group.min_max`: leanprover-community/mathlib4#933 * `algebra.order.group.prod`: leanprover-community/mathlib4#1026 * `algebra.order.group.with_top`: leanprover-community/mathlib4#946 * `algebra.order.hom.monoid`: leanprover-community/mathlib4#944 * `algebra.order.monoid.prod`: leanprover-community/mathlib4#987 * `algebra.order.monoid.to_mul_bot`: leanprover-community/mathlib4#1024 * `algebra.order.ring.abs`: leanprover-community/mathlib4#929 * `algebra.order.ring.cone`: leanprover-community/mathlib4#935 * `algebra.order.sub.basic`: leanprover-community/mathlib4#936 * `algebra.order.sub.with_top`: leanprover-community/mathlib4#932 * `algebra.order.with_zero`: leanprover-community/mathlib4#903 * `combinatorics.quiver.arborescence`: leanprover-community/mathlib4#997 * `combinatorics.quiver.cast`: leanprover-community/mathlib4#990 * `control.traversable.lemmas`: leanprover-community/mathlib4#948 * `data.bool.set`: leanprover-community/mathlib4#960 * `data.int.cast.field`: leanprover-community/mathlib4#1016 * `data.int.cast.lemmas`: leanprover-community/mathlib4#995 * `data.int.cast.prod`: leanprover-community/mathlib4#1015 * `data.int.div`: leanprover-community/mathlib4#1011 * `data.int.dvd.basic`: leanprover-community/mathlib4#996 * `data.int.order.basic`: leanprover-community/mathlib4#938 * `data.nat.cast.basic`: leanprover-community/mathlib4#980 * `data.nat.cast.prod`: leanprover-community/mathlib4#1010 * `data.nat.cast.with_top`: leanprover-community/mathlib4#1019 * `data.nat.gcd.basic`: leanprover-community/mathlib4#965 * `data.nat.order.basic`: leanprover-community/mathlib4#907 * `data.nat.order.lemmas`: leanprover-community/mathlib4#927 * `data.nat.set`: leanprover-community/mathlib4#961 * `data.nat.upto`: leanprover-community/mathlib4#1020 * `data.pequiv`: leanprover-community/mathlib4#1008 * `data.set.basic`: leanprover-community/mathlib4#892 * `data.set.bool_indicator`: leanprover-community/mathlib4#988 * `data.set.image`: leanprover-community/mathlib4#949 * `data.set.n_ary`: leanprover-community/mathlib4#969 * `data.set.opposite`: leanprover-community/mathlib4#983 * `data.set.prod`: leanprover-community/mathlib4#1004 * `data.set.sigma`: leanprover-community/mathlib4#982 * `data.set_like.basic`: leanprover-community/mathlib4#993 * `data.two_pointing`: leanprover-community/mathlib4#984 * `logic.embedding.set`: leanprover-community/mathlib4#986 * `logic.equiv.embedding`: leanprover-community/mathlib4#1021 * `order.directed`: leanprover-community/mathlib4#963 * `order.rel_iso.set`: leanprover-community/mathlib4#1005 * `order.well_founded`: leanprover-community/mathlib4#970 * `ring_theory.coprime.basic`: leanprover-community/mathlib4#899 Co-authored-by: Jireh Loreaux <loreaujy@gmail.com>
mathlib3 655994e298904d7e5bbd1e18c95defd7b543eb94
All remaining issues are elaboration problems involving the order-dual. I think these should be debugged carefully, but I am not sure whether I will have time this weekend, so help is welcome.I fixed these with a bunch of@
and opened a Zulip thread.WithBot
,WithTop
,WithOne
andWithZero
#910