fact: Definition gal_big_prodv_cast_subdef {n} {K : 'I_n -> {subfield L}} (s : gal_of (\big[@prodv_aspace _ _/1%AS]_(i < n) K i)) : {dffun forall i, gal_of (K i)} := [ffun i => normalField_cast (K i) s].
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra) mathcomp(all_solvable all_field) Abel(various char0)