Stream: math-comp users

Topic: Zₚ* cyclic


view this post on Zulip Philipp G. Haselwarter (Jun 22 2023 at 23:29):

For pp prime, Zp×Z_p^\times{} is cyclic ; is this fact recorded somewhere?

view this post on Zulip Cyril Cohen (Jun 23 2023 at 08:44):

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.

view this post on Zulip Cyril Cohen (Jun 23 2023 at 08:58):

There is more general result:

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

view this post on Zulip Cyril Cohen (Jun 23 2023 at 08:59):

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

view this post on Zulip Cyril Cohen (Jun 23 2023 at 09:26):

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.

view this post on Zulip Cyril Cohen (Jun 23 2023 at 10:11):

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


Last updated: Jul 25 2024 at 16:02 UTC