instIsOrderedCancelSMulOfIsOrderedCancelMonoid

English

If G is a commutative monoid with order that is ordered, then IsOrderedCancelSMul G G holds, i.e., left and right cancellation laws respect the order.

Русский

Если G — коммутативный моноид с порядком, удовлетворяющий условию упорядоченной отмены умножения, то IsOrderedCancelSMul G G выполняется: отмена слева и справа согласуется с порядком.

LaTeX

$$IsOrderedCancelSMul G G$$

Lean4

@[to_additive]
instance [CommMonoid G] [PartialOrder G] [IsOrderedCancelMonoid G] : IsOrderedCancelSMul G G
    where
  le_of_smul_le_smul_left _ _ _ := le_of_mul_le_mul_left'
  le_of_smul_le_smul_right _ _ _ := le_of_mul_le_mul_right'

Похожие утверждения