proposition: Lemma inertia_isom phi : 'I_R[cfIsom isoH phi] = g @* 'I_G[phi].
proof: Proof. have [[_ defS] [injg <-]] := (isomP isoH, isomP isoG). rewrite morphimEdom (eq_in_imset eq_hg) -morphimEsub // in defS. rewrite /inertia !setIdE morphimIdom setIA -{1}defS -injm_norm ?injmI //. apply/setP=> gy /[!inE]; apply: andb_id2l => /morphimP[y Gy nHy ->] {gy}. rewrite cfConjgIsom // -sub1set -morphim_set1 // injmSK ?sub1set //= inE. apply/eqP/eqP=> [Iphi_y | -> //]. by apply/cfun_inP=> x Hx; rewrite -!(cfIsomE isoH) ?Iphi_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)