proposition: Lemma dim_fixed_galois K E (G : {group gal_of E}) : galois K E -> G \subset 'Gal(E / K) -> \dim_K (fixedField G) = #|'Gal(E / K) : G|.
proof: Proof. move=> galE sGgal; have [sFE _ _] := and3P galE; apply/eqP. rewrite -divgS // eqn_div ?cardSg // dim_fixedField -galois_dim //. by rewrite mulnC muln_divA ?divnK ?field_dimS ?capvSl -?galois_connection. 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)