mul_left_injective — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[to_additive]
protected theorem mul_left_injective (h : IsUnit b) : Injective (· * b) := fun _ _ => h.mul_right_cancel

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