mathlib

c5128756 - refactor(*): rewrite `to_additive` attribute (#1345)

refactor(*): rewrite `to_additive` attribute (#1345) * chore(algebra/group/to_additive): auto add structure fields * Snapshot * Rewrite `@[to_additive]` * Drop more explicit `name` arguments to `to_additive` * Drop more explicit arguments to `to_additive` * Map namespaces with `run_cmd to_additive.map_namespace` * fix(`group_theory/perm/sign`): fix compile * Fix handling of equational lemmas; fix warnings * Use `list.mmap'`