proposition: Lemma coprime_norm_quotient_pgroup : 'N(T / M) = 'N(T) / M.
proof: Proof. have [-> | ntT] := eqsVneq T 1; first by rewrite quotient1 !norm1 quotientT. have [p_pr _ [m oMpm]] := pgroup_pdiv pT ntT. apply/eqP; rewrite eqEsubset morphim_norms // andbT; apply/subsetP=> Mx. case: (cosetP Mx) => x Nx ->{Mx} nTqMx. have sylT: p.-Sylow(M <*> T) T. rewrite /pHall pT -divgS joing_subr //= norm_joinEr ?coprime_cardMg //. rewrite mulnK // ?p'natE -?prime_coprime // coprime_sym. by rewrite -(@coprime_pexpr m.+1) -?oMpm. have sylTx: p.-Sylow(M <*> T) (T :^ x). have nMTx: x \in 'N(M <*> T). rewrite norm_joinEr // inE -quotientSK ?conj_subG ?mul_subG ?normG //. by rewrite quotientJ // quotientMidl (normP nTqMx). by rewrite pHallE /= -{1}(normP nMTx) conjSg cardJg -pHallE. have{sylT sylTx} [ay] := Sylow_trans sylT sylTx. rewrite /= joingC norm_joinEl //; case/imset2P=> a y Ta. rewrite -groupV => My ->{ay} defTx; rewrite -(coset_kerr x My). rewrite mem_morphim //; first by rewrite groupM // (subsetP (normG M)). by rewrite inE !(conjsgM, defTx) conjsgK conjGid. 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)