mathlib3

011aebd9 - feat(algebra/order/group/defs): add choice-free shortcut instances for `ordered_comm_group` (#17564)