Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-11 08:22 e553f8ad

View on Github →

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.

Estimated changes