smul_left_injective' — Mathlib

English

For a cancellative monoid α, the left action of α on itself is injective (the action is faithful).

Русский

Для моноида с левой отменой α, левое действие α на α является инъективным (верно верное действие).

LaTeX

$$$\\text{Left action is injective: }\\forall a,b\\in\\alpha,\n( a\\cdot x = b\\cdot x\\;\\forall x ) \\Rightarrow a=b.$$$

Lean4

@[to_additive]
theorem smul_left_injective' [SMul M α] [FaithfulSMul M α] : Injective ((· • ·) : M → α → α) := fun _ _ h ↦
  FaithfulSMul.eq_of_smul_eq_smul (congr_fun h)

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