mul_right_injective — Mathlib

English

If a is a unit, then the map x ↦ a·x is injective on the monoid.

Русский

Если a является единичным элементом, тогда отображение x ↦ a·x инъективно на моноиде.

LaTeX

$$$$\forall M [Monoid\ M],\forall a\in M,\ IsUnit(a) \Rightarrow (\forall x,y:\ M,\ a\,x = a\,y \Rightarrow x = y).$$$$

Lean4

@[to_additive]
protected theorem mul_right_injective (h : IsUnit a) : Injective (a * ·) := fun _ _ => h.mul_left_cancel

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