instDistribMulActionSubtypeMem — Mathlib

English

If G acts on α with a DistribMulAction and AddMonoid α, then the restricted action of S on α is DistribMulAction.

Русский

Если G действует на α с DistribMulAction и AddMonoid α, то ограниченное действие S на α является DistribMulAction.

LaTeX

$$$\text{DistribMulAction}(S, \alpha)$$$

Lean4

/-- The action by a subgroup is the action by the underlying group. -/
instance [AddMonoid α] [DistribMulAction G α] (S : Subgroup G) : DistribMulAction S α :=
  inferInstanceAs (DistribMulAction S.toSubmonoid α)

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