feat(group_theory/monoid_localization): Order (#18724)
Prove that every (linearly) ordered cancellative monoid can be embedded into a (linearly) ordered group, namely its Grothendieck group. Note that cancellativity is necessary since submonoids of a group are cancellative.
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
