proposition: Lemma cfuni_tinj s (l : 'P_(m + n)) : '1_[l] (tinj s) = (l == ct s.1 +|+ ct s.2)%:R.
proof: Proof. Proof using. by rewrite cfuniCTnE cycle_type_tinj eq_sym. 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