mathlib3
e7bab9a8 - chore(algebra/group_ring_action/invariant): streamline imports (#18092)

Commit
2 years ago
chore(algebra/group_ring_action/invariant): streamline imports (#18092) 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.
Author
Parents
Loading