mulDistribMulAction — Mathlib

English

The action by a submonoid is the action by the underlying monoid; restricting the action to S yields a consistent action.

Русский

Действие подмонойда есть действие базового моноида; ограничение действия к S даёт согласованное действие.

LaTeX

$$$\text{The action by } S \text{ is the action by the underlying Monoid}$$$

Lean4

/-- The action by a submonoid is the action by the underlying monoid. -/
instance mulDistribMulAction [Monoid α] [MulDistribMulAction M α] (S : Submonoid M) : MulDistribMulAction S α :=
  inferInstance

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