proposition: Lemma mxdirect_sum_kermx n (g : 'M_n) (I : finType) (P : {pred I}) (p_ : I -> {poly K}) : {in P &, forall i j, j != i -> coprimep (p_ i) (p_ j)} -> mxdirect (\sum_(i | P i) kermxpoly g (p_ i))%MS.
proof: Proof. move=> p_coprime; apply/mxdirect_sumsP => i Pi; apply/eqmx0P. have cpNi : {in [pred j | P j && (j != i)] &, forall j k : I, k != j -> coprimep (p_ j) (p_ k)}. by move=> j k /andP[Pj _] /andP[Pk _]; apply: p_coprime. rewrite -!(cap_eqmx (eqmx_refl _) (kermxpoly_prod g _))//. rewrite mxdirect_kermxpoly ?submx_refl//. rewrite (@big_morph _ _ _ true andb) ?big_all_cond ?coprimep1//; last first. by move=> p q; rewrite coprimepMr. by apply/allP => j _; apply/implyP => /andP[Pj neq_ji]; apply: p_coprime. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(div fintype tuple finfun bigop fingroup perm) mathcomp(ssralg zmodp matrix mxalgebra poly polydiv)