proposition: Theorem Frobenius_prime_cent_prime k gT (G K R V : {group gT}) : solvable G -> K ><| R = G -> prime #|R| -> 'C_K(R) = 1 -> k.-abelem V -> G \subset 'N(V) -> k^'.-group G -> #|'C_V(R)| = k -> K^`(1) \subset 'C_K(V).
proof: Proof. move=> solG defG prR regRK abelV nVG k'G primeRV. have [_ sRG _ nKR _] := sdprod_context defG; rewrite subsetI der_sub. have [-> | ntV] := eqsVneq V 1; first exact: cents1. pose rV := abelem_repr abelV ntV nVG. apply: subset_trans (_ : rker rV \subset _); last first. by rewrite rker_abelem subsetIr. have k_pr: prime k by case/pgroup_pdiv: (abelem_pgroup abelV). apply: (Frobenius_prime_rfix1 defG) => //. by rewrite (eq_pgroup G (eq_negn (charf_eq (char_Fp k_pr)))). apply/eqP; rewrite rfix_abelem // -(eqn_exp2l _ _ (prime_gt1 k_pr)). rewrite -{1}(card_Fp k_pr) -card_rowg rowg_mxK. by rewrite card_injm ?abelem_rV_injm ?subsetIl ?primeRV. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq path div) mathcomp(fintype tuple bigop prime binomial finset ssralg fingroup finalg) mathcomp(morphism perm automorphism quotient action commutator gproduct) mathcomp(zmodp cyclic gfunctor center pgroup gseries nilpotent sylow) mathcomp(finmodule abelian frobenius maximal extremal hall) mathcomp(matrix mxalgebra mxrepresentation mxabelem) odd_order(wielandt_fixpoint BGsection1 BGsection2)