Cyclic numbers

TheoremAdditive groups of squarefree order are cyclic#✓fully proved

An additive commutative group of squarefree cardinality is additively cyclic.

theorem IsAddCyclic.of_squarefree_natCard {A : Type*} [AddCommGroup A]
    (hA : Squarefree (Nat.card A)) : IsAddCyclic A

TheoremSzele's criterion for cyclic numbers#✓fully proved

Let \(n\) be a positive integer. Every group of order \(n\) is cyclic if and only if \(n\) is relatively prime to \(\varphi(n)\), that is, \(\gcd(n, \varphi(n)) = 1\), where \(\varphi\) is Euler's totient function.

theorem szele_cyclic_number_criterion
    (n : ℕ) (hn : 0 < n) :
    (∀ (G : Type*) [Group G] [Fintype G], Fintype.card G = n → IsCyclic G) ↔
      Nat.gcd n (Nat.totient n) = 1

Sources

• Joel E. Cohen, "Conjectures about Primes and Cyclic Numbers," Journal of Integer Sequences 28 (2025), Article 25.4.7, Szele's criterion, lines 107–114, https://cs.uwaterloo.ca/journals/JIS/VOL28/Cohen/cohen41.tex (citing T. Szele, "Über die endlichen Ordnungszahlen, zu denen nur eine Gruppe gehört," Comment. Math. Helv. 20 (1947), 265–267).

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.