of_exponent_eq_card — Mathlib

English

If a finite commutative group α satisfies exponent α = card α, then α is cyclic.

Русский

Если конечная коммутативная группа удовлетворяет exp α = |α|, то она циклична.

LaTeX

$$exponent α = Nat.card α → IsCyclic α$$

Lean4

@[to_additive]
theorem of_exponent_eq_card [CommGroup α] [Finite α] (h : exponent α = Nat.card α) : IsCyclic α :=
  let ⟨_⟩ := nonempty_fintype α
  let ⟨g, _, hg⟩ := Finset.mem_image.mp (Finset.max'_mem _ _)
  isCyclic_of_orderOf_eq_card g <| hg.trans <| exponent_eq_max'_orderOf.symm.trans h

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