module

Mathlib.Algebra.Lie.Quotient

URI: https://scilib.ai/kg/mathlib#LieSubmodule.Quotient.module

English

The quotient M/N carries a natural structure of an R-module, induced from the R-module structure of M.

Русский

Фактор-пространство M/N естественно обладает структурой R-модуля, полученной из R-модуля M.

LaTeX

$$$M/N$ is an $R$-module.$$

Lean4

instance module : Module R (M ⧸ N) :=
  Submodule.Quotient.module _

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

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

Разделы

Аффилиация

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