instIsCancelSMulOfIsOrderedCancelSMul

English

If a is ordered cancellative with respect to SMul, then left and right cancellation hold: a • x = a • y imply x = y, and x • a = y • a imply x = y.

Русский

Если умножение на SMul обладает свойством отмены, то левая и правая отмена выполняются: a • x = a • y → x = y и x • a = y • a → x = y.

LaTeX

$$IsCancelSMul G P$$

Lean4

@[to_additive]
instance [PartialOrder G] [PartialOrder P] [SMul G P] [IsOrderedCancelSMul G P] : IsCancelSMul G P
    where
  left_cancel' a b c
    h :=
    (IsOrderedCancelSMul.le_of_smul_le_smul_left a b c h.le).antisymm
      (IsOrderedCancelSMul.le_of_smul_le_smul_left a c b h.ge)
  right_cancel' a b c
    h :=
    (IsOrderedCancelSMul.le_of_smul_le_smul_right a b c h.le).antisymm
      (IsOrderedCancelSMul.le_of_smul_le_smul_right b a c h.ge)

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