mathlib3

2a876b65 - chore(algebra/ordered_group): move monoid stuff to ordered_monoid.lean (#5066)

chore(algebra/ordered_group): move monoid stuff to ordered_monoid.lean (#5066) Replace one 2000 line file with two 1000 line files: ordered group stuff in one, and ordered monoid stuff in the other.