proposition: Lemma isog_nil_class rT G (L : {group rT}) : G \isog L -> nil_class G = nil_class L.
proof: Proof. by case/isogP=> f injf <-; rewrite nil_class_injm. 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)