to_faithfulSMul_mulOpposite — Mathlib

English

A left-cancelative monoid yields a faithful action on the opposite monoid by left action.

Русский

Левостороннее отменяемое моноид обеспечивает верное действие на противоположном моноиде левым действием.

LaTeX

$$$\\text{to_faithfulSMul_mulOpposite }[LeftCancelMonoid \\alpha] : \\text{FaithfulSMul } \\alpha^{\\mathrm{op}} \\alpha$$$

Lean4

/-- `Monoid.toOppositeMulAction` is faithful on cancellative monoids. -/
@[to_additive /-- `AddMonoid.toOppositeAddAction` is faithful on additive cancellative monoids. -/
    ]
instance to_faithfulSMul_mulOpposite [LeftCancelMonoid α] : FaithfulSMul αᵐᵒᵖ α :=
  ⟨fun h ↦ MulOpposite.unop_injective <| mul_left_cancel (h 1)⟩

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