proposition: Lemma inertia_dprod L (phi : 'CF(K)) (psi : 'CF(H)) : L \subset 'N(K) -> L \subset 'N(H) -> phi 1%g != 0 -> psi 1%g != 0 -> 'I_L[cfDprod KxH phi psi] = 'I_L[phi] :&: 'I_L[psi].
proof: Proof. move=> nKL nHL nz_phi nz_psi; apply/eqP; rewrite eqEsubset subsetI. rewrite -{1}(inertia_scale_nz psi nz_phi) -{1}(inertia_scale_nz phi nz_psi). rewrite -(cfDprod_Resl KxH) -(cfDprod_Resr KxH) !sub_inertia_Res //=. by rewrite -inertia_dprodl -?inertia_dprodr // -setIIr setIS ?inertia_mul. 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)