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] - chore: refactor to avoid importing Ring for Group topics #11913
Conversation
Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
(I had more than once traversed these files while creating minimisations, and been annoyed by the spurious imports here!) |
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.
Could you rename Data.Nat.Monoid
/Data.Int.Monoid
to Algebra.Group.Nat
/Algebra.Group.Int
so that those files become clearly algebra?
Nevermind, I split that off to #11924. |
@YaelDillies, I've delegated your #11924. Do you think I could leave it to you to merge master into this, once it is in? |
This PR/issue depends on: |
…hen_talking_about_groups
…hen_talking_about_groups
maintainer merge |
1 similar comment
maintainer merge |
🚀 Pull request has been placed on the maintainer queue by YaelDillies. |
🚀 Pull request has been placed on the maintainer queue by YaelDillies. |
|
||
variable {R : Type*} [Semiring R] (f : R →+* R) (n : ℕ) (x y : R) | ||
|
||
theorem coe_pow (n : ℕ) : ⇑(f ^ n) = f^[n] := |
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.
According to an automated diff, this seems to be the only lemma that disappeared in this PR.
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.
Restored.
bors d+ |
✌️ semorrison can now approve this pull request. To approve and merge a pull request, simply reply with |
bors merge |
This is a far from a complete success at the PR title, but it makes a fair bit of progress, and then guards this with appropriate `assert_not_exists Ring` statements. It also breaks apart the `Mathlib.GroupTheory.Subsemigroup.[Center|Centralizer]` files, to pull the `Set.center` and `Set.centralizer` declarations into their own files not depending on `Subsemigroup`. Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
Build failed: |
…hen_talking_about_groups
bors merge |
This is a far from a complete success at the PR title, but it makes a fair bit of progress, and then guards this with appropriate `assert_not_exists Ring` statements. It also breaks apart the `Mathlib.GroupTheory.Subsemigroup.[Center|Centralizer]` files, to pull the `Set.center` and `Set.centralizer` declarations into their own files not depending on `Subsemigroup`. Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
Pull request successfully merged into master. Build succeeded: |
This is a far from a complete success at the PR title, but it makes a fair bit of progress, and then guards this with appropriate `assert_not_exists Ring` statements. It also breaks apart the `Mathlib.GroupTheory.Subsemigroup.[Center|Centralizer]` files, to pull the `Set.center` and `Set.centralizer` declarations into their own files not depending on `Subsemigroup`. Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
This is a far from a complete success at the PR title, but it makes a fair bit of progress, and then guards this with appropriate `assert_not_exists Ring` statements. It also breaks apart the `Mathlib.GroupTheory.Subsemigroup.[Center|Centralizer]` files, to pull the `Set.center` and `Set.centralizer` declarations into their own files not depending on `Subsemigroup`. Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
This is a far from a complete success at the PR title, but it makes a fair bit of progress, and then guards this with appropriate
assert_not_exists Ring
statements.It also breaks apart the
Mathlib.GroupTheory.Subsemigroup.[Center|Centralizer]
files, to pull theSet.center
andSet.centralizer
declarations into their own files not depending onSubsemigroup
.Data.{Nat,Int}{.Order}.Basic
in group vs ring instances #11924