instMulAction — Mathlib

English

Unitization carries a compatible action of a monoid S acting on R and on A, making it a MulAction over S.

Русский

Unitization имеет совместное действие моноида S на R и A, превращая его в MulAction над S.

LaTeX

$$$[Monoid S] [MulAction S R] [MulAction S A] \\\\Rightarrow MulAction S (Unitization R A).$$$

Lean4

instance instMulAction [Monoid S] [MulAction S R] [MulAction S A] : MulAction S (Unitization R A) :=
  Prod.mulAction

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