proposition: Proposition coprime_abelian_faithful_Ohm1 gT (A G : {group gT}) : A \subset 'N(G) -> coprime #|G| #|A| -> abelian G -> A \subset 'C('Ohm_1(G)) -> A \subset 'C(G).
proof: Proof. move=> nGA coGA cGG; rewrite !(centsC A) => cAG1. have /dprodP[_ defG _ tiRC] := coprime_abelian_cent_dprod nGA coGA cGG. have sRG: [~: G, A] \subset G by rewrite commg_subl. rewrite -{}defG -(setIidPl sRG) TI_Ohm1 ?mul1g ?subsetIr //. by apply/trivgP; rewrite -{}tiRC setIS // subsetI Ohm_sub. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq path div fintype) mathcomp(bigop prime binomial finset fingroup morphism perm automorphism) mathcomp(quotient action gproduct gfunctor commutator) mathcomp(ssralg finalg zmodp cyclic center pgroup finmodule gseries) mathcomp(nilpotent sylow abelian maximal hall extremal) mathcomp(matrix mxalgebra mxrepresentation mxabelem)