isCyclic_units_prime

Mathlib.RingTheory.ZMod.UnitsCyclic

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

English

For prime p, the unit group of ZMod p is cyclic.

Русский

Для простого p единичная группа ZMod p циклична.

LaTeX

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

Lean4

theorem isCyclic_units_prime {p : ℕ} (hp : p.Prime) : IsCyclic (ZMod p)ˣ :=
  have : Fact (p.Prime) := ⟨hp⟩
  inferInstance

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

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

Разделы

Аффилиация

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