proposition: Lemma gal_big_prodv_cast_morphic n (k : {subfield L}) (K : 'I_n -> {subfield L}) : (forall i, galois k (K i)) -> morphic 'Gal((\big[@prodv_aspace _ _/1%AS]_(i < n) K i)%VS / k) gal_big_prodv_cast_subdef.
proof: Proof. rewrite /gal_big_prodv_cast_subdef => galK. apply/'forall_implyP => -[s t]; rewrite inE => /andP[sG tG]. apply/eqP/ffunP => i; rewrite !ffunE/=. have n_gt0 : (n > 0)%N by case: {+}n i => -[]. rewrite (@normalField_castM _ _ _ k) ?galois_normalW//. by rewrite [(k <= _)%VS]galois_subW//= (bigD1 i)//= field_subvMr. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra) mathcomp(all_solvable all_field) Abel(various char0)