proposition: Lemma gal_big_prodv_cast_inj n (k : {subfield L}) (K : 'I_n -> {subfield L}) (galK : forall i, galois k (K i)) : ('injm (gal_big_prodv_cast galK))%g.
proof: Proof. apply/subsetP => /= s s_ker; rewrite inE; apply/gal_eqP => x xK. suff: x \in fixedField [set s]. by move=> /mem_fixedFieldP [_ /(_ s)]; rewrite inE gal_id; apply. apply/subvP: x xK; rewrite /= -[X in (X <= _)%VS]big_prodv_eq_aspace. apply/big_prod_subfieldP => u uK /=; rewrite rpred_prod// => i _. apply/fixedFieldP; first by rewrite (bigD1 i)// -[u i]mulr1 memv_mul ?rpred1 ?uK. move=> s'; rewrite inE => /eqP->{s'}; have /mker := s_ker. rewrite /gal_big_prodv_cast/= morphmE /gal_big_prodv_cast_subdef. move=> /ffunP-/(_ i); rewrite !ffunE. move=> /eqP/gal_eqP/(_ _ (uK _ _))-/(_ isT); rewrite gal_id. rewrite (@normalField_cast_eq _ _ _ k) ?uK ?galois_normalW ?(dom_ker s_ker)//=. 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)