module

Mathlib.Algebra.Module.Submodule.Defs

URI: https://scilib.ai/kg/mathlib#Submodule.module

English

The submodule p inherits an R-module structure from M by restriction of scalars.

Русский

Подмодуль p наследует структуру модуля над R от M посредством ограничения действия скаляра.

LaTeX

$$$Module\ R\ p$$$

Lean4

instance module : Module R p :=
  p.module'

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

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

Разделы

Аффилиация

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