toStarModule — Mathlib

English

A commutative star monoid is a star module over itself via Monoid.toMulAction.

Русский

Коммутативный монойд со звездой образует звездо-модуль над самим собой через действие умножения.

LaTeX

$$$$ \text{StarModule}(R,R). $$$$

Lean4

/-- A commutative star monoid is a star module over itself via `Monoid.toMulAction`. -/
instance toStarModule [CommMonoid R] [StarMul R] : StarModule R R :=
  ⟨star_mul'⟩

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