proposition: Lemma C_prim_root_exists n : (n > 0)%N -> {z : algC | n.-primitive_root z}.
proof: Proof. pose p : {poly algC} := 'X^n - 1; have [r Dp] := closed_field_poly_normal p. move=> n_gt0; apply/sigW; rewrite (monicP _) ?monic_Xn_sub_1 // scale1r in Dp. have rn1: all n.-unity_root r by apply/allP=> z; rewrite -root_prod_XsubC -Dp. have sz_r: (n < (size r).+1)%N. by rewrite -(size_prod_XsubC r id) -Dp size_Xn_sub_1. have [|z] := hasP (has_prim_root n_gt0 rn1 _ sz_r); last by exists z. by rewrite -separable_prod_XsubC -Dp separable_Xn_sub_1 // pnatr_eq0 -lt0n. 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)