isCyclic_units_one

Mathlib.RingTheory.ZMod.UnitsCyclic

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

English

The unit group of ZMod 1 is cyclic.

Русский

Группа единиц ZMod 1 циклична.

LaTeX

$$$ IsCyclic\ ((ZMod\ 1)^{\times}) $$$

Lean4

theorem isCyclic_units_one : IsCyclic (ZMod 1)ˣ :=
  inferInstance

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

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

Разделы

Аффилиация

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