proposition: Fact tinj_morphM : {morph tinj : x y / x * y >-> x * y}.
proof: Proof. Proof using. rewrite /tinj => /= s1 s2; apply /permP => /= x. rewrite permM -(splitK x) !permE. by case: splitP => [] j _; rewrite /tinjval !unsplitK /= permM. 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