instIsRightCancelMul — Mathlib

English

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

Русский

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

LaTeX

$$$\text{IsRightCancelMul}(\alpha) \Rightarrow \text{IsRightCancelMul}(\alpha^{op})$$$

Lean4

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

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