not_isCyclic_units_eight — Mathlib

English

The group of units in the ring Z/8Z is not a cyclic group.

Русский

Группа единиц кольца Z/8Z не циклична.

LaTeX

$$$\\\\neg \\\\IsCyclic\\\\left((\\\\mathbb{Z}/8\\\\mathbb{Z})^{\\\\times}\\\\right).$$$

Lean4

theorem not_isCyclic_units_eight : ¬IsCyclic (ZMod 8)ˣ :=
  by
  rw [IsCyclic.iff_exponent_eq_card, Nat.card_eq_fintype_card, card_units_eq_totient]
  have h : Monoid.exponent (ZMod 8)ˣ ∣ 2 := Monoid.exponent_dvd_of_forall_pow_eq_one (by decide)
  intro (h' : Monoid.exponent (ZMod 8)ˣ = 4)
  simp [h'] at h

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