Theorems · Theorem · group theory

isCyclic_of_card_pow_eq_one_le

∀ {α : Type u_1} [inst : Group α] [inst_1 : DecidableEq α] [inst_2 : Fintype α],
  (∀ (n : ℕ), 0 < n → {a | a ^ n = 1}.card ≤ n) → IsCyclic α

[Stacks Tag 09HX](https://stacks.math.columbia.edu/tag/09HX) (This theorem is stronger than 09HX. It removes the abelian condition, and requires only ≤ instead of =.)

Defined in

Mathlib.GroupTheory.SpecificGroups.Cyclic

Cited by

1 results in Mathlib

Foundations

Depth 102 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

GroupDecidableEqFintype