proposition: Lemma galois_isog (k K F : {subfield L}) : galois k K -> (k <= F)%VS -> 'Gal((K * F) / F) \isog 'Gal (K / K :&: F).
proof: Proof. by move=> galkK /(galois_misom galkK) /misom_isog. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra) mathcomp(all_solvable all_field) Abel(various char0)