proposition: Lemma root_cyclotomic x : root (cyclotomic z n) x = n.-primitive_root x.
proof: Proof. transitivity (x \in [seq z ^+ i | i : 'I_n in [pred i : 'I_n | coprime i n]]). by rewrite -root_prod_XsubC big_image. apply/imageP/idP=> [[k co_k_n ->] | prim_x]. by rewrite prim_root_exp_coprime. have [k Dx] := prim_rootP prim_z (prim_expr_order prim_x). exists (Ordinal (ltn_pmod k n_gt0)) => /=; last by rewrite prim_expr_mod. by rewrite inE coprime_modl -(prim_root_exp_coprime k prim_z) -Dx. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div choice fintype tuple finfun bigop prime) mathcomp(ssralg poly finset fingroup finalg zmodp cyclic) mathcomp(ssrnum ssrint archimedean polydiv intdiv mxpoly) mathcomp(rat vector falgebra fieldext separable galois algC)