toCancelMonoidWithZero — Mathlib

English

If M is a commutative semigroup with zero and right cancellation holds, then left cancellation holds as well.

Русский

Если M — коммутативная полугруппа с нулём и выполняется правое отменение, то выполняется и левое отменение.

LaTeX

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

Lean4

instance (priority := 100) toCancelMonoidWithZero [CancelCommMonoidWithZero M₀] : CancelMonoidWithZero M₀ :=
  { IsLeftCancelMulZero.to_isCancelMulZero (M₀ := M₀) with }

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