Theorems · Theorem · number theory

ZMod.isCyclic_units_iff

∀ (n : ℕ),
  IsCyclic (ZMod n)ˣ ↔ n = 0 ∨ n = 1 ∨ n = 2 ∨ n = 4 ∨ ∃ p m, Nat.Prime p ∧ Odd p ∧ 1 ≤ m ∧ (n = p ^ m ∨ n = 2 * p ^ m)

(ZMod n)ˣ is cyclic iff n is of the form 0, 1, 2, 4, p ^ m, or 2 * p ^ m, where p is an odd prime and 1 ≤ m.

Defined in

Mathlib.RingTheory.ZMod.UnitsCyclic

Cited by

0 results in Mathlib

Foundations

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