proposition: Lemma classic_baseCycloExt (F : fieldType) (n : nat) : (n%:R != 0 :> F) -> classically { L' : splittingFieldType F & { w : L' & <<1; w>>%VS = fullv & n.-primitive_root w }}.
proof: Proof. move=> nN0; suff: classically { L' : fieldExtType F & { w : L' & <<1; w>>%VS = fullv & n.-primitive_root w }}. apply/classic_bind => -[L [w wfull wprim]]; apply/classicW. have splitL : SplittingField.axiom L. exists (cyclotomic w n); rewrite ?cyclotomic_over// -wfull. exact: splitting_Fadjoin_cyclotomic. pose lM := FieldExt_isSplittingField.Build F L splitL. pose lT : splittingFieldType F := HB.pack L lM. by exists lT, w. pose Fo : splittingFieldType F := F^o. apply: classic_bind (@classic_cycloExt _ Fo n nN0). case=> [L [w [iota wfull wprim]]]; apply/classicW. exists L, w => //; apply/eqP; rewrite eqEsubv subvf/= -wfull. apply/subvP => x /Fadjoin_polyP[/= p pover ->]. apply/mempx_Fadjoin/polyOverP => i /=. have /memv_imgP[u _ ->] := polyOverP pover i. by rewrite -(aimg1 iota) memv_img// -regular_fullv memvf. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra) mathcomp(all_solvable all_field) Abel(various cyclotomic_ext)