isCyclic_units_four

Mathlib.RingTheory.ZMod.UnitsCyclic

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

← MathLib Explorer

English

The unit group of ZMod 4 is cyclic.

Русский

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

LaTeX

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

Lean4

theorem isCyclic_units_four : IsCyclic (ZMod 4)ˣ :=
  by
  apply isCyclic_of_prime_card (p := 2)
  simp only [Nat.card_eq_fintype_card, card_units_eq_totient]
  decide
    /- The multiplicative group of `ZMod p` is cyclic. -/

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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