proposition: Lemma Cauchy_homsyms_homsyms : Cauchy_kernel d = \sum_(la : 'P_d) 'hs[la](X) * 'hs[la](Y).
proof: Proof. rewrite Cauchy_homsymm_homsymh. transitivity (\sum_(mu : 'P_d) \sum_(la : 'P_d) 'hm[mu](X) * ('K(la, mu) *: 'hs[la])(Y)). apply eq_bigr => la _. rewrite [X in X(Y)](_ : _ = sympol 'h[la]) //. by rewrite symh_syms -mulr_sumr !linear_sum. rewrite exchange_big /=; apply eq_bigr => la _. have /= -> /= := congr1 val (syms_symm m0 R la). rewrite 2!linear_sum /= mulr_suml; apply eq_bigr => mu _. by rewrite !linearZ /= -scalerAr -scalerAl. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssrint rat ssralg ssrnum algC matrix vector) mathcomp(mpoly) tools partition ordtype antisym Schur_mpoly Schur_altdef sympoly homogsym permcent