instCoeSubmodule

Mathlib.Topology.Algebra.Module.ClosedSubmodule

URI: https://scilib.ai/kg/mathlib#ClosedSubmodule.instCoeSubmodule

English

There is a canonical Coe from ClosedSubmodule R M to Submodule R M, i.e., ClosedSubmodule embeds as a Submodule.

Русский

Существуют канонические переходы Coe из ClosedSubmodule R M в Submodule R M; ClosedSubmodule встроен как подподмодуль.

LaTeX

$$$\text{ClosedSubmodule}(R,M) \hookrightarrow \text{Submodule}(R,M).$$$

Lean4

instance : Coe (ClosedSubmodule R M) (Submodule R M) where coe := toSubmodule

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru