toModule — Mathlib

English

Every submodule of a module is itself a module over the same ring, with scalar multiplication restricted from the ambient module.

Русский

Любой подмодуль модуля является модулем над тем же кольцом, где скалярное умножение ограничено от полного модуля.

LaTeX

$$$ p \text{ is an } R\\text{-module with the restricted action from } M $$$

Lean4

/-- A submodule of a `Module` is a `Module`. -/
instance (priority := 75) toModule : Module R S' :=
  fast_instance%Subtype.coe_injective.module R (AddSubmonoidClass.subtype S') (SetLike.val_smul S')

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