injective_left — Mathlib

English

If an element a is right-cancellable (i.e., right multiplication by a is injective), then the map x ↦ x · a is injective: x · a = y · a implies x = y.

Русский

Если элемент a удовлетворяет свойству правого сокращения, то отображение x ↦ x · a инъективно: x · a = y · a → x = y.

LaTeX

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

Lean4

@[to_additive]
protected theorem injective_left [Mul α] [i : @Std.Commutative α (· * ·)] [PartialOrder α] {a : α}
    (ha : MulLECancellable a) : Injective (· * a) := fun b c h => ha.Injective <| by dsimp; rwa [i.comm a, i.comm a]

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