Commit 2025-02-25 16:16 1477914f

chore: separate the automorphism groups from their tautological action (#22141) There is import tension between monoids of endomorphisms/groups of automorphisms and monoid/group actions:

• end/aut want to import actions to talk about their tautological action on the ground type.
• actions want to import end/aut because an action is the same thing as an hom to the correct end/aut monoid/group Currently, the first bullet point is done in the same file as the definition of end/aut, and the second bullet point is done in files interspersed across the files doing the first bullet point depending on which end/aut monoid/group you're talking about. This is a mess, so this PR makes sure that each of the following are in separate files:
• the definitions of end/aut
• the definition of actions
• the tautological action by end/aut, an action is the same thing as an hom to end/aut

Import replacement guide

Replace imports to your file according to

• Mathlib.Algebra.Group.Aut → Mathlib.Algebra.Group.Action.End
• Mathlib.Algebra.Ring.Aut → Mathlib.Algebra.Ring.Action.End Then run #min_imports.