mathlib
bfe9e712 - chore(algebra/group/defs): fix to_additive instance name (#17079)

Commit
3 years ago
chore(algebra/group/defs): fix to_additive instance name (#17079) This touches a file which is synchronized with mathlib4. One of these mistakes was already indentified in mathlib4. The other is fixed in https://github.com/leanprover-community/mathlib4/pull/481. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Author
Parents
Loading