proposition: Lemma SplittingFieldExt (F0 : fieldType) (L : splittingFieldType F0) (p : {poly F0}) (M : fieldExtType F0) (iota : 'AHom(L, M)) : splittingFieldFor (iota @: fullv) (p ^^ in_alg M) fullv -> SplittingField.axiom M.
proof: Proof. case=> rs pE rsf; have [_/polyOver1P[q ->] [rsq qE rsqf]] := splittingPoly L. exists ((p * q) ^^ in_alg M); first by apply/polyOver1P; exists (p * q). exists (map iota rsq ++ rs); last first. by rewrite adjoin_cat -(aimg1 iota) -aimg_adjoin_seq rsqf rsf. rewrite big_cat/= rmorphM/= big_map mulrC. rewrite (eqp_trans (eqp_mull _ pE))// eqp_mulr//. have := qE; rewrite -(eqp_map iota)/=. rewrite (big_morph _ (rmorphM _) (rmorph1 _))/=. under eq_bigr do rewrite rmorphB/= map_polyX map_polyC/=. by rewrite -map_poly_comp (eq_map_poly (rmorph_alg _)). Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra) mathcomp(all_solvable all_field) Abel(various cyclotomic_ext)