isRightCancelAdd — Mathlib

English

If Mul α and IsRightCancelMul α hold, then Additive α has right-cancellation: a + b = c + b implies a = c.

Русский

Если Mul α и IsRightCancelMul α, то Additive α обладает правой отменой: a + b = c + b ⇒ a = c.

LaTeX

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

Lean4

instance isRightCancelAdd [Mul α] [IsRightCancelMul α] : IsRightCancelAdd (Additive α) :=
  ⟨fun _ _ _ ↦ mul_right_cancel (G := α)⟩

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