proposition: Lemma splitting_Fadjoin_cyclotomic : splittingFieldFor E (cyclotomic w n) <<E; w>>.
proof: Proof. exists [seq w ^+ val k | k <- enum 'I_n & coprime (val k) n]. by rewrite /cyclotomic big_map big_filter big_enum_cond/= eqpxx. rewrite map_comp -(filter_map _ (fun i => coprime i n)) val_enum_ord. have [n_gt1|] := ltnP 1 n; last first. case: n w_is_nth_root (prim_order_gt0 w_is_nth_root) => [|[|]]//= wnth _ _. by rewrite adjoin_seq1 expr0 -[w]expr1 prim_expr_order. set s := (X in <<_ & X>>%VS); suff /eq_adjoin-> : s =i w :: s. rewrite adjoin_cons (Fadjoin_seq_idP _)//. by apply/allP => _/mapP[i _ ->]/=; rewrite rpredX// memv_adjoin. move=> x; rewrite in_cons orbC; symmetry; have []//= := boolP (_ \in _). apply: contraNF => /eqP ->; rewrite -[w]expr1 map_f//. by rewrite mem_filter mem_iota// coprime1n. Qed.
imports: mathcomp(all_ssreflect all_fingroup all_algebra) mathcomp(all_solvable all_field) Abel(char0 various)