proposition: Lemma normal_big_prodv I r (P : {pred I}) (k : {subfield L}) (K : I -> {subfield L}) : (forall i, P i -> normalField k (K i)) -> normalField k (\big[@prodv _ _/1%VS]_(i <- r | P i) K i).
proof: Proof. move=> normkK; elim: r => [|i r IHr]; rewrite !(big_nil, big_cons). apply/normalFieldP => a a1; exists [:: a]; rewrite /= ?a1//. rewrite big_cons big_nil mulr1; apply: minPoly_XsubC. by apply: subvP a1; rewrite sub1v. rewrite big_prodv_eq_aspace in IHr *; case: ifP => // Pi. by rewrite normal_prodv// normkK. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra) mathcomp(all_solvable all_field) Abel(various char0)