instIsLeftCancelMul — Mathlib

English

If α has a right-cancellation property, then the opposite αᵐᵒᵖ has a left-cancellation property.

Русский

Если у α есть свойство правой отмены, то у αᵐᵒᵖ есть свойство левой отмены.

LaTeX

$$$\text{IsLeftCancelMul}(\alpha^{op})$ given $\text{IsRightCancelMul}(\alpha)$$$

Lean4

@[to_additive]
instance instIsLeftCancelMul [Mul α] [IsRightCancelMul α] : IsLeftCancelMul αᵐᵒᵖ where
  mul_left_cancel _ _ _ h := unop_injective <| mul_right_cancel <| op_injective h

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