proposition: Lemma mderivmX m1 m2 : ('X_[m1])^`M[m2] = (\prod_(i < n) (m1 i)^_(m2 i))%:R *: 'X_[m1-m2].
proof: Proof. rewrite [m2]multinomUE_id mderiv_summ filter_predT /index_enum -enumT /=. elim: (enum _) (enum_uniq 'I_n) => /= [|i s ih /andP [i_notin_s uq_s]]. by move=> _; rewrite !big_nil scale1r subm0. pose F j := (m1 j) ^_ (m2 j); rewrite ih // mderivmZ. rewrite big_seq [X in X%:R](eq_bigr F) -?big_seq; last first. move=> j j_in_s; rewrite (bigD1_seq j) //=. rewrite mnmDE mnm_sumE mulmnE mnm1E eqxx mul1n. rewrite big1 ?addn0 // => j' ne_j'j; rewrite mulmnE. by rewrite mnm1E (negbTE ne_j'j). rewrite big_cons mulnC natrM -scalerA; apply/esym. rewrite 2![X in X%:R*:(_*:_)](big_seq, eq_bigr F); last first. move=> j j_in_s; rewrite big_cons mnmDE mnm_sumE. rewrite (bigD1_seq j) //= big1 ?addn0 => [|j' ne_j'j]. rewrite !mulmnE !mnm1E eqxx mul1n; move/memPn: i_notin_s. by rewrite eq_sym => /(_ j j_in_s) /negbTE ->. by rewrite mulmnE mnm1E (negbTE ne_j'j). rewrite -big_seq; congr (_ *: _); rewrite !big_cons. rewrite mnmDE mnm_sumE big_seq big1 ?addn0; last first. move=> /= j j_in_s; rewrite mulmnE mnm1E; move/memPn: i_notin_s. by move/(_ j j_in_s)=> /negbTE->. rewrite mulmnE mnm1E eqxx mul1n; elim: (m2 i)=> /= [|k ihk]. by rewrite ffactn0 scale1r mulm0n add0m mderivm0m. rewrite mderivnS -ihk mderivZ mderivX scalerA -natrM. rewrite submDA Monoid.mulmAC /= mulmSr; congr (_%:R *: 'X_[_]). rewrite mnmBE mnmDE mnm_sumE big_seq big1; last first. move=> /= j j_in_s; rewrite mulmnE mnm1E; move: i_notin_s. by move/memPn/(_ j j_in_s)=> /negbTE->. by rewrite addn0 mulmnE mnm1E eqxx mul1n ffactnSr. 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