proposition: Lemma isog_center (aT rT : finGroupType) (G : {group aT}) (H : {group rT}) : G \isog H -> 'Z(G) \isog 'Z(H).
proof: Proof. exact: gFisog. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient action gproduct gfunctor) mathcomp(cyclic)