proposition: Lemma prim_root_natf_neq0 (F : fieldType) n (w : F) : n.-primitive_root w -> (n%:R != 0 :> F).
proof: Proof. have [->//|n_gt0] := posnP n => x_prim; apply/negPf/negP => nFneq0. have /natf0_char[//|p char_p] := nFneq0. have p_prime : prime p := charf_prime char_p. move: nFneq0; rewrite -(dvdn_charf char_p) => dvdpn. have [k cpk nE] := pfactor_coprime p_prime n_gt0. have k_gt0 : (k > 0)%N by move: n_gt0; rewrite nE muln_gt0 => /andP[]. have /prim_expr_order/eqP := x_prim; rewrite nE exprM. elim: (logn p n) => [|i IHi]; last first. rewrite expnSr exprM -subr_eq0 -Frobenius_autE -(Frobenius_aut1 char_p). by rewrite -rmorphB fmorph_eq0 subr_eq0. rewrite -(prim_order_dvd x_prim) nE mulnC Gauss_dvd ?coprimeXl//. rewrite pfactor_dvdn// ltn_geF// -[k]muln1 logn_Gauss ?logn1//. by rewrite logn_gt0 mem_primes p_prime dvdpn n_gt0. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra all_solvable) mathcomp(all_field)