isLeftCancelAdd — Mathlib

English

If α is a semigroup with left-cancellation property, then Additive α inherits left-cancellation: a + b = a + c implies b = c.

Русский

Если α имеет левую отмену, то Additive α наследует левую отмену: a + b = a + c ⇒ b = c.

LaTeX

$$Additive isLeftCancelAdd: ∀ a,b,c, a + b = a + c → b = c$$

Lean4

instance isLeftCancelAdd [Mul α] [IsLeftCancelMul α] : IsLeftCancelAdd (Additive α) :=
  ⟨@mul_left_cancel α _ _⟩

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