Cyclicity of (ZMod n)ˣ in Mathlib

Stream: Is there code for X?

[hooyuser]

I’d like to know whether mathlib already contains the classification of when the unit group of ZMod n is cyclic. Concretely, I’m after the statement:

Theorem. (ZMod n)ˣ is cyclic if and only if
  • n = 1, 2, 4, or
  • n = p^k, or
  • n = 2 * p^k,

where p is an odd prime and k > 0.

In particular I need the “if” direction. Thanks in advance for pointers!

[Kenny Lau]

from a brief loogle search it doesn't seem like we have all the facts you want.

[Kenny Lau]

it seems like we only know that it's cyclic for n=p

[Edison Xie]

Do we have the existence of primitive roots?

[Kenny Lau]

Edison Xie said:

Do we have the existence of primitive roots?

isn't that the same question?

[Filippo A. E. Nuccio]

@Antoine Chambert-Loir has something on this, no?

[Antoine Chambert-Loir]

Indeed, i have formalized this last week. I'll push a PR fork or whatever soon. (Note that it is also cyclic for n = 0 .) This is #25879

[hooyuser]

Antoine Chambert-Loir said:

Indeed, i have formalized this last week. I'll push a PR fork or whatever soon. (Note that it is also cyclic for n = 0 .) This is #25879

Thanks for doing this! I’ve had a look at PR #25879 and the proof looks great. Looking forward to seeing it merged into mathlib soon.

[Junyan Xu]

I made this a student project in our course this semester, but no one took it :)

[Yaël Dillies]

(this link 404s, probably because your repo is private)

[Junyan Xu]

Thanks, this is it in the web editor.