proposition: Lemma classic_cycloExt (F0 : fieldType) (L : fieldExtType F0) n : (n%:R != 0 :> F0) -> classically { L' : fieldExtType F0 & { w : L' & { iota : 'AHom(L, L') | <<iota @: fullv; w>>%VS = fullv & n.-primitive_root w }}}.
proof: Proof. case: n => [|[_|[two_neq0|n']]]//; first by rewrite eqxx. - apply/classicW; exists L, 1, (id_ahom _); rewrite ?prim_root1//. by rewrite lim1g (Fadjoin_idP _)// rpred1. - apply/classicW; exists L, (- 1), (id_ahom _) => /=. by rewrite lim1g (Fadjoin_idP _)// rpredN1. by rewrite prim2_rootN1// -(rmorph_nat (in_alg L)) fmorph_eq0. set n := n'.+3 => nF0neq0. have poly_XnsubC_neq0 : 'X^n - 1 != 0 :> {poly L}. by rewrite -size_poly_eq0 size_XnsubC. apply: classic_bind (classic_fieldExtFor (poly_XnsubC_neq0)). case=> [L' [rs [iota rs_full]]]. rewrite rmorphB rmorph1/= map_polyXn. rewrite eqp_monic ?monic_XnsubC ?monic_prod_XsubC// => /eqP Xnsub1E. have rs_uniq : uniq rs. rewrite -separable_prod_XsubC -Xnsub1E separable_Xn_sub_1//. have: in_alg L' n%:R != 0 by rewrite fmorph_eq0. by rewrite raddfMn/= -(@in_algE _ L') rmorph1. have rs_ge : (n <= size rs)%N. have /(congr1 (fun p : {poly _} => size p)) := Xnsub1E. rewrite size_XnsubC// size_prod_seq; last first. by move=> i _; rewrite polyXsubC_eq0. under eq_bigr do rewrite size_XsubC. rewrite big_tnth sum_nat_const card_ord subSn ?leq_pmulr//. by rewrite muln2 -addnn addnK => -[->]. have rsUroots : all n.-unity_root rs. apply/allP => r rrs; apply/eqP; rewrite Xnsub1E. by rewrite (big_rem _ rrs)/= hornerM hornerXsubC subrr mul0r. have /has_prim_root/(_ _ _)/hasP[]// := rsUroots. move=> w wrs wprim; apply/classicW; exists L', w, iota => //. symmetry; rewrite -rs_full; have /eq_adjoin-> : rs =i w :: rs. by move=> r'; rewrite in_cons; case: eqVneq => // -> /=. set K := limg iota => {wrs rs_uniq Xnsub1E rs_full rs_ge}. elim: rs rsUroots => [|r' rs IHrs /andP[r'Uroots rsUroots]]. by rewrite adjoin_seq1. have r'K : r' \in <<K; w>>%VS. have /unity_rootP/(prim_rootP wprim)[i ->] := r'Uroots. by rewrite rpredX// memv_adjoin. by rewrite !adjoin_cons (Fadjoin_idP r'K) -adjoin_cons IHrs. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra) mathcomp(all_solvable all_field) Abel(various cyclotomic_ext)