proposition: Fact group_set_inertia (H : {group gT}) phi : group_set 'I[phi : 'CF(H)].
proof: Proof. apply/group_setP; split; first by rewrite inE group1 /= cfConjgJ1. move=> y z /setIdP[nHy /eqP n_phi_y] /setIdP[nHz n_phi_z]. by rewrite inE groupM //= cfConjgMnorm ?n_phi_y. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype div tuple finfun bigop prime order) mathcomp(ssralg ssrnum finset fingroup morphism perm) mathcomp(automorphism quotient action zmodp cyclic center) mathcomp(gproduct commutator gseries nilpotent pgroup) mathcomp(sylow maximal frobenius matrix mxalgebra) mathcomp(mxrepresentation vector algC classfun character) mathcomp(archimedean)