instMulDistribMulActionSubtypeMem

English

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

Русский

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

LaTeX

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

Lean4

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

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