proposition: Lemma gal_fixedField E (G : {group gal_of E}): 'Gal(E / fixedField G) = G.
proof: Proof. apply/esym/eqP; rewrite eqEcard galois_connection_subset /= (dim_fixedField G). rewrite galois_dim //; apply/galois_fixedField/eqP. rewrite eqEsubv galois_connection_subv ?capvSl //. by rewrite fixedFieldS ?galois_connection_subset. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(choice fintype tuple finfun bigop ssralg poly) mathcomp(polydiv finset fingroup morphism quotient perm) mathcomp(action zmodp cyclic matrix mxalgebra vector) mathcomp(falgebra fieldext separable)