isCancelAdd — Mathlib

English

If α is a type with multiplication that is cancelable, then the additive structure on α is cancellative; i.e., for all a, b, c in α, a + b = a + c implies b = c.

Русский

Пусть α имеет умножение, для которого выполняется отмена; тогда над α определение сложения имеет отмену: для любых a, b, c ∈ α, если a + b = a + c, то b = c.

LaTeX

$$$[Mul\,\alpha] \land [IsCancelMul\,\alpha] \Rightarrow IsCancelAdd(\text{Additive }\alpha)$$$

Lean4

instance isCancelAdd [Mul α] [IsCancelMul α] : IsCancelAdd (Additive α) :=
  ⟨⟩

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