instIsRightCancelMulZeroOfIsLeftCancelMulZero

English

If α has Multiplication, Zero, and IsLeftCancelMulZero, then αᵐᵒᵖ has IsRightCancelMulZero.

Русский

Если у α есть умножение, ноль и левое отменяющее умножение на ноль, то у αᵐᵒᵖ есть правое отменяющее умножение на ноль.

LaTeX

$$MulOpposite.instIsRightCancelMulZeroOfIsLeftCancelMulZero$$

Lean4

instance [Mul α] [Zero α] [IsLeftCancelMulZero α] : IsRightCancelMulZero αᵐᵒᵖ where
  mul_right_cancel_of_ne_zero h _ _
    eq := unop_injective <| mul_left_cancel₀ (unop_injective.ne_iff.mpr h) (congr_arg unop eq)

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