proposition: Theorem odd_prime_sdprod_abelem_cent1 k gT (G K R V : {group gT}) : solvable G -> odd #|G| -> K ><| R = G -> coprime #|K| #|R| -> prime #|R| -> k.-abelem V -> G \subset 'N(V) -> k^'.-group G -> 'C_V(R) = 1 -> [~: R, K] \subset 'C_K(V).
proof: Proof. move=> solG oddG defG coKR prR abelV nVG k'G regR. have [_ sRG _ nKR _] := sdprod_context defG; rewrite subsetI commg_subr nKR. case: (eqsVneq V 1) => [-> | ntV]; first exact: cents1. pose rV := abelem_repr abelV ntV nVG. apply: subset_trans (_ : rker rV \subset _); last first. by rewrite rker_abelem subsetIr. apply: odd_prime_sdprod_rfix0 => //. have k_pr: prime k by case/pgroup_pdiv: (abelem_pgroup abelV). by rewrite (eq_pgroup G (eq_negn (charf_eq (char_Fp k_pr)))). by apply/eqP; rewrite -submx0 rfix_abelem //= regR morphim1 rowg_mx1. 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)