instAddActionSubtypeMem — Mathlib

English

The induced action by a submodule on a module coincides with the ambient action restricted to that submodule.

Русский

Индуцированное действие подмодуля на модуль совпадает с ограниченным действием над подмодулем.

LaTeX

$$$\text{AddAction}_{p\subset M} = \text{AddAction}_{M|p}$$$

Lean4

/-- The action by a submodule is the action by the underlying module. -/
instance [AddAction M α] : AddAction p α :=
  AddAction.compHom _ p.subtype.toAddMonoidHom

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