toOpposite_starModule — Mathlib

English

A commutative star monoid is a star module over its opposite via a canonical action.

Русский

Коммутативный звёздовый полугруппа является звёздовым модулем над своим противоположным через каноническое действие.

LaTeX

$$$\text{If } R \text{ is a commutative star monoid, then } R^{\mathrm{op}} \text{ acts as a StarModule on } R.$$$

Lean4

/-- A commutative star monoid is a star module over its opposite via
`Monoid.toOppositeMulAction`. -/
instance toOpposite_starModule [CommMonoid R] [StarMul R] : StarModule Rᵐᵒᵖ R :=
  ⟨fun r s => star_mul' s r.unop⟩

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