proposition: Lemma muni_is_multiplicative : multiplicative muni.
proof: Proof. apply/commr_mmap_is_multiplicative=> /= [i p|p m1 m2]. rewrite /X; case: splitP=> j _; last exact/commr_polyX. by apply/polyP=> k; rewrite coefCM coefMC; apply/commr_mpolyX. apply/polyP=> k; rewrite coefCM coefMC XE coefZ coefXn. case: eqP; rewrite ?(mulr0, mul0r, mulr1, mul1r) //= => _. exact/commr_mpolyX. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype tuple finfun bigop finset binomial) mathcomp(order fingroup perm ssralg zmodp poly ssrint) mathcomp(matrix vector) mathcomp(bigenough) ssrcomplements freeg