proposition: Lemma classic_cycloSplitting (F0 : fieldType) (L : splittingFieldType F0) n : (n%:R != 0 :> F0) -> classically { L' : splittingFieldType F0 & { w : L' & { iota : 'AHom(L, L') | <<iota @: fullv; w>>%VS = fullv & n.-primitive_root w }}}.
proof: Proof. move=> /(@classic_cycloExt _ L). apply/classic_bind => -[M [w [iota wfull wprim]]]; apply/classicW. suff splitM : SplittingField.axiom M. pose mM := FieldExt_isSplittingField.Build F0 M splitM. pose mT : splittingFieldType F0 := HB.pack M mM. by exists mT, w, iota. apply: (@SplittingFieldExt _ L ('Phi_n ^^ intr) _ iota). rewrite -map_poly_comp (eq_map_poly (rmorph_int _)) -wfull. by rewrite (Phi_cyclotomic wprim); apply: splitting_Fadjoin_cyclotomic. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra) mathcomp(all_solvable all_field) Abel(various cyclotomic_ext)