Skip to content
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(algebra/group_ring_action/invariant): streamline imports #18092

Closed
wants to merge 5 commits into from

Conversation

hrmacbeth
Copy link
Member

@hrmacbeth hrmacbeth commented Jan 7, 2023

The only file importing algebra/group_ring_action/invariant was algebra/hom/group_action. This means that the material needing both files can safely be moved from hom/group_action to group_ring_action/invariant, while only decreasing the imports of anything else in the hierarchy.

This is worth doing since group_ring_action/invariant has another relatively heavy import (ring_theory/subring/pointwise). After this rearrangement, hom/group_action should be ready to port.


Open in Gitpod

@hrmacbeth hrmacbeth changed the title Hrmacbeth hom group action chore(algebra/group_ring_action/invariant): streamline imports Jan 7, 2023
@hrmacbeth hrmacbeth added the awaiting-CI The author would like to see what CI has to say before doing more work. label Jan 7, 2023
@github-actions github-actions bot removed the awaiting-CI The author would like to see what CI has to say before doing more work. label Jan 8, 2023
@hrmacbeth hrmacbeth added the awaiting-review The author would like community review of the PR label Jan 8, 2023
@dupuisf
Copy link
Collaborator

dupuisf commented Jan 8, 2023

Thanks!

bors r+

@github-actions github-actions bot added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed awaiting-review The author would like community review of the PR labels Jan 8, 2023
bors bot pushed a commit that referenced this pull request Jan 8, 2023
The only file importing `algebra/group_ring_action/invariant` was `algebra/hom/group_action`.  This means that the material needing both files can safely be moved from `hom/group_action` to `group_ring_action/invariant`, while only decreasing the imports of anything else in the hierarchy.

This is worth doing since `group_ring_action/invariant` has another relatively heavy import (`ring_theory/subring/pointwise`).  After this rearrangement, `hom/group_action` should be ready to port.
@bors
Copy link

bors bot commented Jan 8, 2023

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title chore(algebra/group_ring_action/invariant): streamline imports [Merged by Bors] - chore(algebra/group_ring_action/invariant): streamline imports Jan 8, 2023
@bors bors bot closed this Jan 8, 2023
@bors bors bot deleted the hrmacbeth-hom-group-action branch January 8, 2023 07:57
Copy link
Member

@eric-wieser eric-wieser left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks! I think I ran out of steam when moving things into invariant.lean and decided to leave the remaining lemmas until the mathlib4 tide got close enough to motivate moving them!

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.)
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

3 participants