Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-10 21:17 84cbbc98

View on Github →

feat(algebra/group/to_additive + a few more files): make to_additive convert unit to add_unit (#12564) This likely involves removing names that match autogenerated names.

Estimated changes