instMulAction — Mathlib

English

Let G be a group acting on α. Then for any subgroup S ≤ G, there is a natural MulAction of S on α given by restricting the G-action to S.

Русский

Пусть G действует на α. Тогда для любой подсвязи S ≤ G существует естественное действие S на α, получаемое ограничением действия G до S.

LaTeX

$$$\text{MulAction } S \; \alpha\; \text{ (restriction of the G-action to } S\text{)}$$

Lean4

/-- The action by a subgroup is the action by the underlying group. -/
@[to_additive /-- The additive action by an add_subgroup is the action by the underlying `AddGroup`. -/
    ]
instance instMulAction : MulAction S α :=
  inferInstanceAs (MulAction S.toSubmonoid α)

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