inj — Mathlib

English

Let α be a type with a binary operation that is cancellable on the left for a fixed element a. Then for all b,c in α, a · b = a · c if and only if b = c.

Русский

Пусть α — множество с бинарной операцией и существует такое свойство, что умножение слева на a сокращает. Тогда для любых b,c в α верно: a · b = a · c тогда и только тогда b = c.

LaTeX

$$$MulLECancellable(a) \rightarrow (a \cdot b = a \cdot c \iff b = c)$$$

Lean4

@[to_additive]
protected theorem inj [Mul α] [PartialOrder α] {a b c : α} (ha : MulLECancellable a) : a * b = a * c ↔ b = c :=
  ha.Injective.eq_iff

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