Commit 2026-04-17 17:11 9f48cac6

View on Github →

chore(GroupTheory/GroupAction/Hom): improve to_additive use (#38150) This PR cleans up after #34249, replacing some uses of to_additive existing with just to_additive. The fields of MulDistribMulAction had to be reordered in order to align with the additive version DistribMulAction. This is an adaptation for the overlapping instances linter (#38126)

Estimated changes