Commit 2025-06-29 08:52 f8aa277c

feat:(RingTheory/ZMod/CyclicUnits): characterize when (ZMod n)ˣ is cyclic (#26020) Prove that the group (ZMod n)ˣ is cyclic iff one of the following mutually exclusive cases happens:

• n = 0 (then ZMod 0 ≃+* ℤ and the group of units is cyclic of order 2);
• n = 1, 2 or 4
• n is a power p ^ e of an odd prime number, or twice such a power (with 1 ≤ e). Some individual cases are proved in passing and are also directly provided by (n= 0, 1, 2, 4, 8, prime, prime powers). This is a new PR of #25879 after the migration via fork. See that PR for the preceding discussion.