proposition: Lemma kermxpoly_prod 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)} -> (kermxpoly g (\prod_(i | P i) p_ i) :=: \sum_(i | P i) kermxpoly g (p_ i))%MS.
proof: Proof. move=> p_coprime; elim: index_enum (index_enum_uniq I). by rewrite !big_nil ?kermxpoly1 ?submx_refl//. move=> j js ihjs /= /andP[jNjs js_uniq]; apply/eqmxP. rewrite !big_cons; case: ifP => [Pj|PNj]; rewrite ?ihjs ?submx_refl//. suff cjjs: coprimep (p_ j) (\prod_(i <- js | P i) p_ i). by rewrite !kermxpolyM// !(adds_eqmx (eqmx_refl _) (ihjs _)) ?submx_refl. rewrite (@big_morph _ _ _ true andb) ?big_all_cond ?coprimep1//; last first. by move=> p q; rewrite coprimepMr. apply/allP => i i_js; apply/implyP => Pi; apply: p_coprime => //. by apply: contraNneq jNjs => <-. 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)