mathlib
55bbb807 - chore(algebra/order/group): Restore basic instances (#17810)

Commit
3 years ago
chore(algebra/order/group): Restore basic instances (#17810) Moving the inheritance instances results in unexpected and confusing errors when importing `algebra.order.group.defs` but not `algebra.order.group.instances`. This puts the inheritance instances back into `algebra.order.group.defs`.
Author
Parents
Loading