mkQ

Mathlib.LinearAlgebra.FreeModule.ModN

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

English

The quotient map G → G/nG is the canonical projection ModN G n.

Русский

Картежная проекция G → G/nG является каноническим отображением в ModN G n.

LaTeX

$$mkQ : G →+ ModN G n$$

Lean4

/-- The quotient map `G → G / nG`. -/
def mkQ : G →+ ModN G n :=
  (LinearMap.range (LinearMap.lsmul ℤ G n)).mkQ

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

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

Разделы

Аффилиация

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