mathlib3
44e2d1e4 - chore(algebra/support): golf, use `to_additive` (#17711)

Commit

3 years ago

chore(algebra/support): golf, use `to_additive` (#17711)

Author

urkud

urkud

Parents

Loading