ModN

Mathlib.LinearAlgebra.FreeModule.ModN

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

English

The quotient of a group G by the subgroup of n-multiples is denoted ModN G n.

Русский

Фактор-группа G/(nG) обозначается как ModN G n.

LaTeX

$$ModN G n := G ⧸ range (lsmul ℤ G n)$$

Lean4

/-- `ModN G n` denotes the quotient of `G` by multiples of `n` -/
abbrev ModN : Type _ :=
  G ⧸ LinearMap.range (LinearMap.lsmul ℤ G n)

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

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

Разделы

Аффилиация

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