proposition: Lemma injm_ucn n G : 'injm f -> G \subset D -> f @* 'Z_n(G) = 'Z_n(f @* G).
proof: Proof. exact: injmF. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(fintype div bigop prime finset fingroup morphism) mathcomp(automorphism quotient commutator gproduct) mathcomp(gfunctor center gseries cyclic)