instModuleZMod

Mathlib.LinearAlgebra.FreeModule.ModN

URI: https://scilib.ai/kg/mathlib#ModN.instModuleZMod

English

There is a natural module structure of ZMod n on ModN G n, turning ModN G n into a ZMod n-module.

Русский

Для ModN G n существует естественная структура модуля ZMod n, превращающая ModN G n в модуль ZMod n.

LaTeX

$$ModN G n is a module over ZMod n$$

Lean4

instance : Module (ZMod n) (ModN G n) :=
  QuotientAddGroup.zmodModule (by simp)

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

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

Разделы

Аффилиация

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