proposition: Lemma charsimple_solvable G : charsimple G -> solvable G -> is_abelem G.
proof: Proof. case/charsimple_dprod=> H [sHG simH [I Aut_I defG]] solG. have p_pr: prime #|H| by apply: simple_sol_prime (solvableS sHG solG) simH. set p := #|H| in p_pr; apply/is_abelemP; exists p => //. elim/big_rec: _ (G) defG => [_ <-|f B If IH_B M defM]; first exact: abelem1. have [Af [[_ K _ defB] _ _ _]] := (subsetP Aut_I f If, dprodP defM). rewrite (dprod_abelem p defM) defB IH_B // andbT -(autmE Af) -morphimEsub //=. rewrite morphim_abelem ?abelemE // exponent_dvdn. by rewrite cyclic_abelian ?prime_cyclic. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(div fintype finfun bigop finset prime binomial) mathcomp(fingroup morphism perm automorphism quotient) mathcomp(action commutator gproduct gfunctor ssralg) mathcomp(countalg finalg zmodp cyclic pgroup center gseries) mathcomp(nilpotent sylow abelian finmodule)