proposition: Lemma card_linear_irr (sG : irrType G) : [char F]^'.-group G -> group_splitting_field G -> #|linear_irr sG| = #|G : G^`(1)|%g.
proof: Proof. move=> F'G splitG; apply/eqP. wlog sGq: / irrType (G / G^`(1))%G by apply: socle_exists. have [_ nG'G] := andP (der_normal 1 G); apply/eqP; rewrite -card_quotient //. have cGqGq: abelian (G / G^`(1))%g by apply: sub_der1_abelian. have F'Gq: [char F]^'.-group (G / G^`(1))%g by apply: morphim_pgroup. have splitGq: group_splitting_field (G / G^`(1))%G. exact: quotient_splitting_field. rewrite -(sum_irr_degree sGq) // -sum1_card. pose rG (j : sGq) := morphim_repr (socle_repr j) nG'G. have irrG j: mx_irreducible (rG j) by apply/morphim_mx_irr; apply: socle_irr. rewrite (reindex (fun j => irr_comp sG (rG j))) /=. apply: eq_big => [j | j _]; last by rewrite irr_degree_abelian. have [_ lin_j _ _] := rsim_irr_comp sG F'G (irrG j). by rewrite inE -lin_j -irr_degreeE irr_degree_abelian. pose sGlin := {i | i \in linear_irr sG}. have sG'k (i : sGlin) : G^`(1)%g \subset rker (irr_repr (val i)). by case: i => i /= /[!inE] lin; rewrite rker_linear //=; apply/eqP. pose h' u := irr_comp sGq (quo_repr (sG'k u) nG'G). have irrGq u: mx_irreducible (quo_repr (sG'k u) nG'G). by apply/quo_mx_irr; apply: socle_irr. exists (fun i => oapp h' [1 sGq]%irr (insub i)) => [j | i] lin_i. rewrite (insubT [in _] lin_i) /=; apply/esym/eqP/socle_rsimP. apply: mx_rsim_trans (rsim_irr_comp sGq F'Gq (irrGq _)). have [g lin_g inj_g hom_g] := rsim_irr_comp sG F'G (irrG j). exists g => [||G'x]; last 1 [case/morphimP=> x _ Gx ->] || by []. by rewrite quo_repr_coset ?hom_g. rewrite (insubT (mem _) lin_i) /=; apply/esym/eqP/socle_rsimP. set u := Sub i lin_i; apply: mx_rsim_trans (rsim_irr_comp sG F'G (irrG _)). have [g lin_g inj_g hom_g] := rsim_irr_comp sGq F'Gq (irrGq u). exists g => [||x Gx]; last 1 [have:= hom_g (coset _ x)] || by []. by rewrite quo_repr_coset; first by apply; rewrite mem_quotient. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div choice fintype tuple finfun bigop prime) mathcomp(ssralg poly polydiv finset fingroup morphism) mathcomp(perm automorphism quotient finalg action zmodp) mathcomp(commutator cyclic center pgroup matrix mxalgebra) mathcomp(mxpoly)