English
Any linearly ordered commutative group is an ordered cancel monoid; namely, le_of_mul_le_mul_left and le_of_mul_le_mul_right hold in such a structure.
Русский
Любая линейно упорядоченная коммутативная группа является упорядоченным отменяемым моноидом: выполняются неравенства le_of_mul_le_mul_left и le_of_mul_le_mul_right.
LaTeX
$$$\text{IsOrderedCancelMonoid}(\alpha)$ given $(\alpha$ is a commutative group, partially ordered, and IsOrderedMonoid$)$$$
Lean4
@[to_additive IsOrderedAddMonoid.toIsOrderedCancelAddMonoid]
instance (priority := 100) toIsOrderedCancelMonoid [CommGroup α] [PartialOrder α] [IsOrderedMonoid α] :
IsOrderedCancelMonoid α
where
le_of_mul_le_mul_left a b c bc := by simpa using mul_le_mul_left' bc a⁻¹
le_of_mul_le_mul_right a b c bc := by simpa using mul_le_mul_left' bc a⁻¹
