proposition: Lemma center_aut_extraspecial k : coprime k p -> exists2 f, f \in Aut S & forall z, z \in 'Z(S) -> f z = (z ^+ k)%g.
proof: Proof. have /cyclicP[z defZ]: cyclic 'Z(S) by rewrite prime_cyclic ?oZ. have oz: #[z] = p by rewrite orderE -defZ. rewrite coprime_sym -unitZpE ?prime_gt1 // -oz => u_k. pose g := Zp_unitm (FinRing.unit 'Z_#[z] u_k). have AutZg: g \in Aut 'Z(S) by rewrite defZ -im_Zp_unitm mem_morphim ?inE. have ZSfull := Aut_sub_fullP (center_sub S) Aut_extraspecial_full. have [f [injf fS fZ]] := ZSfull _ (injm_autm AutZg) (im_autm AutZg). exists (aut injf fS) => [|u Zu]; first exact: Aut_aut. have [Su _] := setIP Zu; have z_u: u \in <[z]> by rewrite -defZ. by rewrite autE // fZ //= autmE permE /= z_u /cyclem expg_znat. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(div fintype finfun bigop finset prime binomial) mathcomp(fingroup morphism perm automorphism quotient) mathcomp(action commutator gproduct gfunctor ssralg) mathcomp(countalg finalg zmodp cyclic pgroup center gseries) mathcomp(nilpotent sylow abelian finmodule)