For $p$ prime, $Z_p^\times{}$ is cyclic ; is this fact recorded somewhere?

I can only find that `units_Zp`

is abelian in the library... ~~it looks like the cyclicity result is missing. You're welcome to contribute it.~~

There is more general result:

```
Lemma field_unit_group_cyclic [F : finFieldType] (G : {group {unit F}}) : cyclic G
```

Any subgroup of the units of a finite field is cyclic.

There is one subtlety (about changing the type from `'F_p`

to `'Z_p`

:

```
Lemma units_Zp_cyclic p : prime p -> cyclic (units_Zp p).
Proof.
move=> p_prime; suff: cyclic [set: {unit 'F_p}] by rewrite pdiv_id.
exact: field_unit_group_cyclic.
Qed.
```

https://github.com/math-comp/math-comp/pull/1041

Last updated: Jul 25 2024 at 16:02 UTC