mathlib

b02bf9a6 - refactor(algebra/order/monoid/basic): splits defs and basic