-
Notifications
You must be signed in to change notification settings - Fork 310
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(Algebra/Regular/Basic): port file #758
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.
LGTM: I don't think the to_additive
issue is a problem at all (it just means the default translation wasn't baked into to_additive
), and in this case I think a type ascription is reasonable, even if Lean 3 managed to avoid it.
It seems to be just a matter of putting them in the right place. I hope you don't mind that I just pushed that to your branch :) |
bors merge |
mathlib SHA: 76171581280d5b5d1e2d1f4f37e5420357bdc636 Porting notes: 1. It seems like `to_additive` is not correctly converting `IsLeftRegular`, `IsRightRegular`, and `IsRegular`. Giving explicit names for their conversion fixes this issue. 2. The proof of `IsLeftRegular.ne_zero` needed an additional type annotation to behave properly Co-authored-by: Jireh Loreaux <loreaujy@gmail.com> Co-authored-by: Jon Eugster <Jon.Eugster@hhu.de>
Pull request successfully merged into master. Build succeeded: |
* master: (26 commits) docs (Order.BoundedOrder): fix typos (#775) feat: port Algebra.Order.Monoid.Cancel.Defs (#774) feat: port Order.Disjoint (#773) feat: port linarith (#526) feat: port Algebra.Order.Monoid.Defs (#771) feat: port control.functor (#612) feat(Algebra/GroupWithZero/Commute): port file (#762) feat: port Logic.Equiv.Option (#674) chore: fix todos in `to_additive` (#765) feat(Algebra/Order/Monoid/MinMax): port file (#763) fix: update context in recursive calls in split_ifs (#761) feat(Algebra/Regular/Basic): port file (#758) feat: port Order.BoundedOrder (#697) feat: port Data.Pi.Algebra (#564) feat: port Algebra.Hom.Embedding (#764) fix: to_additive generates equation lemmas for target (#767) fix: fix translation errors in various files (#716) fix: remove submodules (#766) feat(Algebra/Group/Commute): port file (#750) feat(Algebra/Ring/Commute): port file (#759) ...
Regenerated from the [port status wiki page](https://github.com/leanprover-community/mathlib/wiki/mathlib4-port-status). Relates to the following PRs: * `algebra.field.defs`: leanprover-community/mathlib4#668 * `algebra.group.commute`: leanprover-community/mathlib4#750 * `algebra.group_with_zero.commute`: leanprover-community/mathlib4#762 * `algebra.group_with_zero.semiconj`: leanprover-community/mathlib4#757 * `algebra.group_with_zero.units.basic`: leanprover-community/mathlib4#735 * `algebra.hom.embedding`: leanprover-community/mathlib4#764 * `algebra.order.monoid.cancel.defs`: leanprover-community/mathlib4#774 * `algebra.order.monoid.canonical.defs`: leanprover-community/mathlib4#778 * `algebra.order.monoid.defs`: leanprover-community/mathlib4#771 * `algebra.order.monoid.min_max`: leanprover-community/mathlib4#763 * `algebra.order.monoid.order_dual`: leanprover-community/mathlib4#786 * `algebra.order.sub.defs`: leanprover-community/mathlib4#732 * `algebra.regular.basic`: leanprover-community/mathlib4#758 * `algebra.ring.commute`: leanprover-community/mathlib4#759 * `algebra.ring.regular`: leanprover-community/mathlib4#795 * `algebra.ring.semiconj`: leanprover-community/mathlib4#751 * `control.applicative`: leanprover-community/mathlib4#798 * `control.functor`: leanprover-community/mathlib4#612 * `control.monad.basic`: leanprover-community/mathlib4#752 * `data.countable.defs`: leanprover-community/mathlib4#736 * `data.int.units`: leanprover-community/mathlib4#807 * `data.nat.basic`: leanprover-community/mathlib4#729 * `data.nat.psub`: leanprover-community/mathlib4#806 * `data.nat.units`: leanprover-community/mathlib4#805 * `data.pi.algebra`: leanprover-community/mathlib4#564 * `data.prod.lex`: leanprover-community/mathlib4#783 * `logic.embedding.basic`: leanprover-community/mathlib4#700 * `logic.equiv.option`: leanprover-community/mathlib4#674 * `order.bounded_order`: leanprover-community/mathlib4#697 * `order.with_bot`: leanprover-community/mathlib4#776 * `order.disjoint`: leanprover-community/mathlib4#773 * `order.min_max`: leanprover-community/mathlib4#728 * `order.prop_instances`: leanprover-community/mathlib4#792 * `order.rel_iso.basic`: leanprover-community/mathlib4#772
mathlib SHA: 76171581280d5b5d1e2d1f4f37e5420357bdc636
Porting notes:
to_additive
is not correctly convertingIsLeftRegular
,IsRightRegular
, andIsRegular
. Giving explicit names for their conversion fixes this issue.IsLeftRegular.ne_zero
needed an additional type annotation to behave properly