proposition: Lemma isom_tinj : isom SnXm (tinj @* ('dom tinj)) tinj.
proof: Proof. Proof using. apply/isomP; split; last by []. apply/subsetP => [] /= [s1 s2]; rewrite inE => /andP[_]. rewrite !inE /= => /eqP/permP H. rewrite -[1]/(1,1) /xpair_eqE /=. apply/andP; split; apply/eqP/permP => x; rewrite !perm1. - have:= H (unsplit (inl x)). by rewrite permE /tinjval unsplitK perm1 /=; apply: lshift_inj. - have:= H (unsplit (inr x)). by rewrite permE /tinjval unsplitK perm1 /=; apply: rshift_inj. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssralg fingroup morphism perm gproduct) mathcomp(ssrnum matrix vector mxalgebra algC) mathcomp(classfun character mxrepresentation) tools ordcast partition sorted permcomp cycles cycletype permcent