proposition: Lemma sub_cent_Puig_at n p G : n > 0 -> p.-group G -> 'C_G('L_{n}(G)) \subset 'L_{n}(G).
proof: Proof. move=> n_gt0 pG. have /ex_maxgroup[M /(max_SCN pG)SCN_M]: exists M, (gval M <| G) && abelian M. by exists 1%G; rewrite normal1 abelian1. have{SCN_M} [cMM [nsMG defCM]] := (SCN_abelian SCN_M, SCN_P SCN_M). have sML: M \subset 'L_{n}(G) by apply: abelian_norm_Puig. by apply: subset_trans (sML); rewrite -defCM setIS // centS. 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)