to_isCancelMulZero — Mathlib

English

If a left-cancellation property holds, then the structure is cancellative in the sense of IsCancelMulZero.

Русский

Если выполняется левое отменение, то структура обладает свойством отмены по нулю слева и справа.

LaTeX

$$$\text{IsLeftCancelMulZero}(M_0) \Rightarrow \text{IsCancelMulZero}(M_0)$$$

Lean4

theorem to_isCancelMulZero [IsLeftCancelMulZero M₀] : IsCancelMulZero M₀ :=
  { IsLeftCancelMulZero.to_isRightCancelMulZero with }

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