toIsCancelMul — Mathlib

English

In an ordered cancellative monoid, multiplication is cancellative: if a b = a c, then b = c; similarly on the right.

Русский

В упорядоченном(cancel) моноиде с отменой умножения: если a b = a c, то b = c; аналогично слева и справа.

LaTeX

$$a b = a c \Rightarrow b = c \,\land\, b a = c a \Rightarrow b = c$$

Lean4

@[to_additive]
instance (priority := 100) toIsCancelMul : IsCancelMul α
    where
  mul_left_cancel _ _ _ h := (le_of_mul_le_mul_left' h.le).antisymm <| le_of_mul_le_mul_left' h.ge
  mul_right_cancel _ _ _ h := (le_of_mul_le_mul_right' h.le).antisymm <| le_of_mul_le_mul_right' h.ge

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