proposition: Lemma img_gal_big_prodv_cast_sub n (k : {subfield L}) (K : 'I_n -> {subfield L}) (galK : forall i, galois k (K i)) (E := (\big[@prodv_aspace _ _/1%AS]_(i < n) K i)%AS) (G := 'Gal(E / k)%g): (gal_big_prodv_cast galK @* G \subset setXn (fun i => 'Gal(K i / k)))%g.
proof: Proof. case: n => [|n] in K galK E G *. rewrite setX0; apply/subsetP => /= x _; rewrite !inE. by apply/eqP/ffunP => -[]. apply/subsetP => /= x; rewrite !inE morphimEdom => /imsetP[s sG ->]/=. apply/forallP => i/=; rewrite morphmE/= ffunE/=. rewrite -(@normalField_img _ _ E)// ?galois_normalW//. - by rewrite (galois_subW (galK _))//= /E (bigD1 i)//= field_subvMr. - by move=> ? ?/=; rewrite mem_morphim//. - by rewrite /E/= -big_prodv_eq_aspace galois_big_prodv//= card_ord. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra) mathcomp(all_solvable all_field) Abel(various char0)