mathlib3

a5ce41d8 - refactor(algebra/order/group/basic): split