For prime, 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: Oct 13 2024 at 01:02 UTC