to_additive): monadic code cosmetics (#12527)

Commit

3 years ago

refactor(algebra/group/to_additive): monadic code cosmetics (#12527) as suggested by @kmill and @eric-wieser, but the merge was faster Also improve test file.

Author

nomeata

Parents

47b1ddf2

mathlib e553f8ad - refactor(algebra/group/to_additive): monadic code cosmetics (#12527)

mathlib
e553f8ad - refactor(algebra/group/to_additive): monadic code cosmetics (#12527)