mathlib

59b9ebb1 - feat(algebra/group/to_additive): customize the relevant argument (#9138)

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.