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: ring covariance & ordered ring typeclasses for WithBot
#1508
Conversation
Note: the mathlib3 PR is still open right now. |
LGTM bors d+ (not merging, because I think it might conflict with some other PRs that I just put on the queue; feel free to merge after an hour or so) |
✌️ negiizhao can now approve this pull request. To approve and merge a pull request, simply reply with |
…eclasses for `with_bot` (#18149) mathlib4 PR: leanprover-community/mathlib4#1508
bors merge |
mathlib3 PR: leanprover-community/mathlib#18149 Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com>
Pull request successfully merged into master. Build succeeded: |
WithBot
WithBot
Update some SHAs of files that changed in mathlib3. These 17 files need mainly only updated SHA as they've been only touched by backports or already have been forward-ported. The relevant changes are: * [Algebra.Group.Defs (#17884)](https://leanprover-community.github.io/mathlib-port-status/file/algebra/group/defs?range=41cf0cc2f528dd40a8f2db167ea4fb37b8fde7f3..2e0975f6a25dd3fbfb9e41556a77f075f6269748) * #945 * [Algebra.Group.WithOne.Defs (#18081)](https://leanprover-community.github.io/mathlib-port-status/file/algebra/group/with_one/defs?range=e574b1a4e891376b0ef974b926da39e05da12a06..995b47e555f1b6297c7cf16855f1023e355219fb) * #1439 * [Algebra.Module.Submodule.Basic (#18291) : backport](https://leanprover-community.github.io/mathlib-port-status/file/algebra/module/submodule/basic?range=f7fc89d5d5ff1db2d1242c7bb0e9062ce47ef47c..feb99064803fd3108e37c18b0f77d0a8344677a3) * [Algebra.Order.Monoid.WithTop (#18149, #18081)](https://leanprover-community.github.io/mathlib-port-status/file/algebra/order/monoid/with_top?range=2258b40dacd2942571c8ce136215350c702dc78f..e7e2ba8aa216a5833b5ed85a93317263711a36b5) * #1508 * #1439 * [Algebra.Order.Ring.WithTop (#18149, #18081)](https://leanprover-community.github.io/mathlib-port-status/file/algebra/order/ring/with_top?range=550b58538991c8977703fdeb7c9d51a5aa27df11..e7e2ba8aa216a5833b5ed85a93317263711a36b5) * #1508 * #1439 * [Data.Finset.NAry (#18081)](https://leanprover-community.github.io/mathlib-port-status/file/data/finset/n_ary?range=9003f28797c0664a49e4179487267c494477d853..995b47e555f1b6297c7cf16855f1023e355219fb) * #1439 * [Data.Option.NAry (#18081)](https://leanprover-community.github.io/mathlib-port-status/file/data/option/n_ary?range=2258b40dacd2942571c8ce136215350c702dc78f..995b47e555f1b6297c7cf16855f1023e355219fb) * #1439 * [Data.Set.NAry (#18081)](https://leanprover-community.github.io/mathlib-port-status/file/data/set/n_ary?range=2ed7e4aec72395b6a7c3ac4ac7873a7a43ead17c..995b47e555f1b6297c7cf16855f1023e355219fb) * #1439 * [Data.SetLike.Basic (#18291) : backport](https://leanprover-community.github.io/mathlib-port-status/file/data/set_like/basic?range=fc2ed6f838ce7c9b7c7171e58d78eaf7b438fb0e..feb99064803fd3108e37c18b0f77d0a8344677a3) * [Data.Sum.Basic (#18184)](https://leanprover-community.github.io/mathlib-port-status/file/data/sum/basic?range=d6aae1bcbd04b8de2022b9b83a5b5b10e10c777d..f4ecb599422baaf39055d8278c7d9ef3b5b72b88) * #1583 * [GroupTheory.GroupAction.SubMulAction (#18291) : backport](https://leanprover-community.github.io/mathlib-port-status/file/group_theory/group_action/sub_mul_action?range=f93c11933efbc3c2f0299e47b8ff83e9b539cbf6..feb99064803fd3108e37c18b0f77d0a8344677a3) * [GroupTheory.Submonoid.Basic (#18291) : backport](https://leanprover-community.github.io/mathlib-port-status/file/group_theory/submonoid/basic?range=207cfac9fcd06138865b5d04f7091e46d9320432..feb99064803fd3108e37c18b0f77d0a8344677a3) * [ Logic.Basic (#18291): backport](https://leanprover-community.github.io/mathlib-port-status/file/logic/basic?range=1c521b4fb909320eca16b2bb6f8b5b0490b1cb5e..feb99064803fd3108e37c18b0f77d0a8344677a3) * #1509 * [Order.InitialSeg (#18198): backport](https://leanprover-community.github.io/mathlib-port-status/file/order/initial_seg?range=ee0c179cd3c8a45aa5bffbf1b41d8dbede452865..7c3269ca3fa4c0c19e4d127cd7151edbdbf99ed4) * [Order.RelClasses (#17957)](https://leanprover-community.github.io/mathlib-port-status/file/order/rel_classes?range=c4658a649d216f57e99621708b09dcb3dcccbd23..bc7d81beddb3d6c66f71449c5bc76c38cb77cf9e) * #1047 * [Order.WithBot (#18081)](https://leanprover-community.github.io/mathlib-port-status/file/order/with_bot?range=70d50ecfd4900dd6d328da39ab7ebd516abe4025..995b47e555f1b6297c7cf16855f1023e355219fb) * #1439 * [RingTheory.Subsemiring.Basic (#18291) : backport](https://leanprover-community.github.io/mathlib-port-status/file/ring_theory/subsemiring/basic?range=f93c11933efbc3c2f0299e47b8ff83e9b539cbf6..feb99064803fd3108e37c18b0f77d0a8344677a3) Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
mathlib3 PR: leanprover-community/mathlib#18149