Commit 2021-09-25 04:13 59b9ebb1

feat(algebra/group/to_additive): customize the relevant argument (#9138) @[to_additive] now automatically checks for each declaration what the first argument is with a multiplicative structure on it. This is now the argument that is tested when executing later occurrences of @[to_additive] for a fixed type to decide whether this declaration should be translated or not.