proposition: Lemma galois_dim K E : galois K E -> \dim_K E = #|'Gal(E / K)|.
proof: Proof. case/and3P=> sKE /eq_adjoin_separable_generator-> // nKE. set a := separable_generator K E in nKE *. have [r /allP/=Er splitKa] := normalFieldP nKE a (memv_adjoin K a). rewrite (dim_sup_field (subv_adjoin K a)) mulnK ?adim_gt0 //. apply/eqP; rewrite -eqSS -adjoin_degreeE -size_minPoly splitKa size_prod_XsubC. set n := size r; rewrite eqSS -[n]card_ord. have x_ (i : 'I_n): {x | x \in 'Gal(<<K; a>> / K) & x a = r`_i}. apply/sig2_eqW/normalField_root_minPoly; rewrite ?subv_adjoin ?memv_adjoin //. by rewrite splitKa root_prod_XsubC mem_nth. have /card_image <-: injective (fun i => s2val (x_ i)). move=> i j /eqP; case: (x_ i) (x_ j) => y /= galEy Dya [z /= galEx Dza]. rewrite gal_adjoin_eq // Dya Dza nth_uniq // => [/(i =P j)//|]. by rewrite -separable_prod_XsubC -splitKa; apply: separable_generatorP. apply/eqP/eq_card=> x; apply/codomP/idP=> [[i ->] | galEx]; first by case: x_. have /(nthP 0) [i ltin Dxa]: x a \in r. rewrite -root_prod_XsubC -splitKa. by rewrite root_minPoly_gal ?memv_adjoin ?subv_adjoin. exists (Ordinal ltin); apply/esym/eqP. by case: x_ => y /= galEy /eqP; rewrite Dxa gal_adjoin_eq. 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)