proposition: Lemma msym_comp_poly k (p : {mpoly R[n]}) (t : n.-tuple {mpoly R[k]}) : p \is symmetric -> (forall s : 'S_k, perm_eq t [tuple (msym s t`_i) | i < n]) -> p \mPo t \is symmetric.
proof: Proof. move=> sym_p sym_t; apply/issymP=> s; pose_big_enough l. rewrite (comp_mpolywE _ (w := l)) //. 2: by close. case/tuple_permP: (sym_t s^-1)%g => s' tE. pose F (m : 'X_{1..n < l}) := insubd m [multinom m (s' i) | i < n]. have FE m: F m = [multinom m (s' i) | i < n] :> 'X_{1..n}. by rewrite insubdK // -topredE /= mdeg_mperm ?bmdeg. rewrite raddf_sum {1}(reindex_inj (h := F)) /=; last first. move=> m1 m2 /(congr1 (@bmnm _ _)); rewrite !FE. by move/mperm_inj=> /val_inj. apply/eq_bigr=> m _; rewrite linearZ /= FE msym_coeff //. rewrite rmorph_prod /= (reindex_inj (perm_inj (s := s'^-1))) /=. congr (_ *: _); apply/eq_bigr=> i _; rewrite rmorphXn /=. rewrite mnmE permKV (tnth_nth 0) {1}tE -!tnth_nth. rewrite !tnth_map !tnth_ord_tuple permKV -msymMm. by rewrite mulVg msym1m -tnth_nth. 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