subtype — Mathlib

English

If A acts on a module and A is a substructure of M, the induced action of A on a module coincides with the action of M restricted to A.

Русский

Если A действует на модуль и A является подструктурой M, то индуцированное действие A на модуль совпадает с действием M, ограниченным на A.

LaTeX

$$$\text{Action}_{A} = \text{Action}_{M|A}$$$

Lean4

/-- The natural `R`-linear map from a submodule of an `R`-module `M` to `M`. -/
protected def subtype : S' →ₗ[R] M where
  toFun := Subtype.val
  map_add' _ _ := rfl
  map_smul' _ _ := rfl

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