instIsLeftCancelMulZeroOfIsRightCancelMulZero

English

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

Русский

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

LaTeX

$$MulOpposite.instIsLeftCancelMulZeroOfIsRightCancelMulZero$$

Lean4

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

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