proposition: Lemma splitting_num_field (p : {poly rat}) : {L : splittingFieldType rat & { LtoC : {rmorphism L -> algC} | (p != 0 -> splittingFieldFor 1 (p ^^ in_alg L) {:L}) /\ (p = 0 -> L = [the splittingFieldType rat of rat^o]) }}.
proof: Proof. have [->|p_neq0] := eqVneq p 0; first by exists rat^o, ratr; split. have [/= rsalg pE] := closed_field_poly_normal (p ^^ (ratr : _ -> algC)). have {}pE : p ^^ ratr %= \prod_(z <- rsalg) ('X - z%:P). by rewrite pE (eqp_trans (eqp_scale _ _)) ?eqpxx// lead_coef_eq0 map_poly_eq0. have [L' [L'toC [rs' rs'E rs'f]]] := num_field_exists rsalg. have splitL' : splittingFieldFor 1 (p ^^ in_alg L') {: L'}%AS. exists rs' => //; rewrite -(eqp_map L'toC). by rewrite -map_poly_comp map_prod_XsubC rs'E (eq_map_poly (fmorph_eq_rat _)). have splitaxL' : SplittingField.axiom L'. by exists (p ^^ in_alg L'); first by apply/polyOver1P; exists p. pose Frat := [the fieldType of rat : Type]. pose sM' := FieldExt_isSplittingField.Build Frat L' splitaxL'. pose S' : splittingFieldType Frat := HB.pack L' sM'. exists S', L'toC; split => //. by move=> p_eq0; rewrite p_eq0 eqxx in p_neq0. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra) mathcomp(all_solvable all_field polyrcf) Abel(various classic_ext map_gal algR) Abel(char0 cyclotomic_ext real_closed_ext)