fact: Definition normalClosure (U V : {vspace L}) := (\big[@prodv _ _/1]_(s in kAEndf U) (s @: (U * V)))%VS.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra) mathcomp(all_solvable all_field) Abel(various char0)