to_isLeftCancelMulZero — Mathlib

English

In a commutative semigroup with zero, right-cancellation implies left-cancellation.

Русский

В коммутативной полугруппе с нулём правое отменение влечёт за собой левое отменение.

LaTeX

$$$\text{IsRightCancelMulZero}(M_0) \Rightarrow \text{IsLeftCancelMulZero}(M_0)$ in a commutative setting with zero.$$

Lean4

theorem to_isLeftCancelMulZero [IsRightCancelMulZero M₀] : IsLeftCancelMulZero M₀ :=
  {
    mul_left_cancel_of_ne_zero := fun hb _ _ h =>
      mul_right_cancel₀ hb <| (mul_comm _ _).trans (h.trans (mul_comm _ _)) }

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