smul_left_cancel — Mathlib

English

Let a be a unit in a monoid α acting on β. Then left-multiplication by a is injective on β; equivalently, for all x,y ∈ β, a • x = a • y implies x = y.

Русский

Пусть a является единицей в моноиде α, действует на β. Тогда левое умножение на a инъективно на β; то есть для любых x,y ∈ β верно a • x = a • y ⇒ x = y.

LaTeX

$$$ a \in \alpha^{\times} \Rightarrow \forall x,y \in \beta,\ a \cdot x = a \cdot y \Leftrightarrow x = y. $$$

Lean4

@[to_additive]
theorem smul_left_cancel {a : α} (ha : IsUnit a) {x y : β} : a • x = a • y ↔ x = y :=
  let ⟨u, hu⟩ := ha
  hu ▸ smul_left_cancel_iff u

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