Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-01-08 05:18 e7bab9a8

View on Github →

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.

Estimated changes