proposition: Lemma trivg_center_Puig_pgroup p G : p.-group G -> 'Z('L(G)) = 1 -> G :=: 1.
proof: Proof. move=> pG LG1; apply/(trivg_center_pgroup pG)/trivgP. rewrite -(trivg_center_pgroup (pgroupS (Puig_sub _) pG) LG1). by apply: subset_trans (sub_cent_Puig pG); apply: sub_center_cent_Puig_at. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq div) mathcomp(fintype bigop prime finset ssralg fingroup morphism) mathcomp(automorphism quotient gfunctor commutator zmodp center pgroup) mathcomp(sylow gseries nilpotent abelian maximal) mathcomp(matrix mxalgebra mxrepresentation mxabelem) odd_order(BGsection1 BGsection2)