English
Let α be a nontrivial cancellative monoid with zero. Then the left action of the opposite monoid αᵐᵒᵖ on α by multiplication is faithful; equivalently, the map αᵐᵒᵖ → End(α) given by aᵐᵒᵖ ↦ (x ↦ a x) is injective.
Русский
Пусть α — ненулевой отменимый моноид с нулём. Тогда левое действие противоположного моноида αᵐᵒᵖ на α по умножению тождественно различает элементы: отображение aᵐᵒᵖ ↦ (x ↦ a x) инъективно.
LaTeX
$$$\text{The map }\alpha^{op} \to \mathrm{End}(\alpha),\; a^{op} \mapsto (x \mapsto a x)$ is injective, provided $\alpha$ is a nontrivial cancellative monoid with zero.$$
Lean4
/-- `Monoid.toOppositeMulAction` is faithful on nontrivial cancellative monoids with zero. -/
instance toFaithfulSMul_opposite [CancelMonoidWithZero α] [Nontrivial α] : FaithfulSMul αᵐᵒᵖ α :=
⟨fun h => unop_injective <| mul_left_cancel₀ one_ne_zero (h 1)⟩
