proposition: Lemma morphim_p_rank_abelian p G : abelian G -> 'r_p(f @* G) <= 'r_p(G).
proof: Proof. move=> cGG; have sHG := subsetIr D G; apply: leq_trans (p_rankS p sHG). have cHH := abelianS sHG cGG; rewrite -morphimIdom /=; set H := D :&: G. have sylP := nilpotent_pcore_Hall p (abelian_nil cHH). have sPH := pHall_sub sylP. have sPD: 'O_p(H) \subset D by rewrite (subset_trans sPH) ?subsetIl. rewrite -(p_rank_Sylow (morphim_pHall f sPD sylP)) -(p_rank_Sylow sylP) //. rewrite -!rank_pgroup ?morphim_pgroup ?pcore_pgroup //. by rewrite morphim_rank_abelian ?(abelianS sPH). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path choice) mathcomp(div fintype finfun bigop finset prime binomial) mathcomp(fingroup morphism perm automorphism action) mathcomp(quotient gfunctor gproduct ssralg countalg finalg zmodp) mathcomp(cyclic pgroup gseries nilpotent sylow)