instIsAddCyclicInt

Mathlib.GroupTheory.SpecificGroups.Cyclic

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

English

For any n, the additive group ZMod n is cyclic; generated by 1.

Русский

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

LaTeX

$$IsAddCyclic (ZMod n)$$

Lean4

instance : IsAddCyclic ℤ :=
  ⟨1, fun n ↦ ⟨n, by simp only [smul_eq_mul, mul_one]⟩⟩

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

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

Разделы

Аффилиация

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