mulAction — Mathlib

English

The action by a submonoid is the action by the underlying monoid.

Русский

Действие подмонойда на множестве совпадает с действием исходного моноида.

LaTeX

$$$\text{MulAction } S \ α$ where $S = \text{Submonoid } M'$ and action is inherited from $M'$.$$

Lean4

/-- The action by a submonoid is the action by the underlying monoid. -/
@[to_additive /-- The additive action by an `AddSubmonoid` is the action by the underlying `AddMonoid`. -/
    ]
instance mulAction [MulAction M' α] (S : Submonoid M') : MulAction S α :=
  inferInstance

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