proposition: Lemma dim_fixedField E (G : {group gal_of E}) : #|G| = \dim_(fixedField G) E.
proof: Proof. have [w [_ nzw] [_ Edirect /(_ (groupP G))defE]] := gal_matrix G. set n := #|G|; set m := \dim (fixedField G); rewrite -defE (directvP Edirect). rewrite -[n]card_ord -(@mulnK #|'I_n| m) ?adim_gt0 //= -sum_nat_const. congr (_ %/ _)%N; apply: eq_bigr => i _. by rewrite dim_cosetv ?(memPn nzw) ?mem_tnth. 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)