proposition: Lemma prim_root1 (F : fieldType) n : (n.-primitive_root (1 : F)) = (n == 1)%N.
proof: Proof. case: n => [|[|n]]//. by apply/'forall_eqP => i; rewrite ord1//= eqxx; apply/unity_rootP. apply/'forall_eqP => /= /(_ (@Ordinal _ n _))/=/(_ _)/unity_rootP. by rewrite !ltnS leqnSn ltn_eqF//; apply => //; rewrite expr1n. Qed.
imports: mathcomp(all_ssreflect all_fingroup all_algebra) mathcomp(all_solvable all_field) Abel(char0 various)