instMulAction — Mathlib

English

If M is a monoid and α is a set with an action of M, then the Lex M-monoid acts on α by the same action.

Русский

Если M — моноид и на множества α задано действие M, то у Lex M существует аналогичное действие на α, заданное тем же правилом.

LaTeX

$$$ \\text{Monoid}(M) \\wedge \\text{MulAction}(M, \\alpha) \\Rightarrow \\text{MulAction}(\\mathrm{Lex}\\,M, \\alpha). $$$

Lean4

@[to_additive]
instance instMulAction [Monoid M] [MulAction M α] : MulAction (Lex M) α :=
  ‹MulAction M α›

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