Commit 2026-05-27 15:09 f4093103

refactor(GroupTheory/*): additivize AddAut (#39884) Currently AddAut is a multiplicative group, which prevents arguments in group theory using the conjugation action G →* MulAut G from being to_additivized (because a correct additivization would require inserting Additive around AddAut G and dealing with these extra Additives in the proof, but to_additive is unable to do this automatically). So currently any such conjugation argument in group theory must be duplicated for additive groups. This PR fixes this by additivizing AddAut. This also means switching the existing DistribMulAction of AddAut A on A to a new typeclass AddDistribAddAction. I've included a some initial cleanup in Algebra/Group/Subgroup/Basic and Algebra/Group/Subgroup/Pointwise, but there is plenty more that will have to wait for future PRs. Zulip thread: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/MulAut.20and.20to_additive