proposition: Lemma Fchar_inv_is_linear : linear Fchar_inv.
proof: Proof. Proof using. move=> a f g; rewrite !Fchar_invE scaler_sumr -big_split /=. apply eq_bigr => la _. by move: ('1z_[la]) => U; rewrite !linearD !linearZ /= scalerDl scalerA mulrC. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism gproduct) mathcomp(rat ssralg ssrint ssrnum algC vector archimedean) mathcomp(mxrepresentation classfun character) mathcomp(mpoly) sorted ordtype tools partition antisym sympoly homogsym Cauchy Schur_altdef stdtab therule permcomp cycletype towerSn permcent reprSn unitriginv MurnaghanNakayama