-
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.Hom.Group #659
Conversation
Along with module, class, and some lemma docstrings I kept the additional later-file defns near the bottom Turns out this file doesn't rely on the Logic.Nontrivial import
…efs' into winstonyin
This reverts commit 698f6ec.
…to pechersky/port-group-with-zero-defs
That's fixed, but now blocked by leanprover/lean4#1907. |
I think I've now killed off all the porting notes (baring one about to_additive). This PR uses a forked version of Lean 4 until nightly-2022-12-03 is available. It will be broken until aesop gets updated in leanprover-community/aesop#32. (Edit: aesop updated.) |
bors merge |
👎 Rejected by label |
bors merge |
mathlib3 SHA: 8c53048add6ffacdda0b36c4917bfe37e209b0ba - [x] depends on #563 - [x] depends on leanprover-community/mathlib#17733 - [x] depends on leanprover/lean4#1901 - [x] depends on leanprover/lean4#1907 Co-authored-by: Winston Yin <winstonyin@gmail.com> Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Jireh Loreaux <loreaujy@gmail.com> Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Pull request successfully merged into master. Build succeeded: |
mathlib3 SHA: 76171581280d5b5d1e2d1f4f37e5420357bdc636 Seems relatively straightforward. Some lemma names (e.g. `units.coe_zpow -> Units.val_zpow_eq_zpow_val`) are renamed to refer to `val` instead of `coe`, following the convention used in `Algebra.Group.Units`. - [x] depends on: #659 Co-authored-by: Winston Yin <winstonyin@gmail.com> Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Jireh Loreaux <loreaujy@gmail.com> Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Regenerated from the [port status wiki page](https://github.com/leanprover-community/mathlib/wiki/mathlib4-port-status). Relates to the following PRs: * `algebra.divisibility.basic`: leanprover-community/mathlib4#833 * `algebra.group.with_one.defs`: leanprover-community/mathlib4#841 * `algebra.hom.commute`: leanprover-community/mathlib4#831 * `algebra.hom.group`: leanprover-community/mathlib4#659 * `algebra.hom.units`: leanprover-community/mathlib4#745 * `algebra.ring.basic`: leanprover-community/mathlib4#830 * `category_theory.natural_isomorphism`: leanprover-community/mathlib4#820 * `combinatorics.quiver.connected_component`: leanprover-community/mathlib4#836 * `combinatorics.quiver.subquiver`: leanprover-community/mathlib4#828 Co-authored-by: Johan Commelin <johan@commelin.net>
mathlib3 SHA: 8c53048add6ffacdda0b36c4917bfe37e209b0ba