instIsAddCyclic

Mathlib.GroupTheory.SpecificGroups.Cyclic

URI: https://scilib.ai/kg/mathlib#ZMod.instIsAddCyclic

English

For every n, ZMod n has a cyclic additive group structure.

Русский

Для каждого n, ZMod n имеет циклическую аддитивную структуру.

LaTeX

$$ZMod.instIsAddCyclic$$

Lean4

instance instIsAddCyclic (n : ℕ) : IsAddCyclic (ZMod n) :=
  isAddCyclic_of_surjective (Int.castRingHom _) ZMod.intCast_surjective

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

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

Разделы

Аффилиация

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