proposition: Lemma mcoeff_sym p (s : 'S_n) m : (msym s p)@_m = p@_(m#s).
proof: Proof. pose_big_enough i; first rewrite (msymE s i) //. apply/esym; rewrite {1}[p](mpolywE (k := i)) //. rewrite !raddf_sum /=; apply/eq_bigr=> j _. rewrite !mcoeffZ !mcoeffX; congr (_ * _). have bijF: bijective (fun (m : 'X_{1..n}) => m#(s^-1)%g). exists (fun (m : 'X_{1..n}) => m#s) => m'. + by apply/mnmP=> k; rewrite !mnmE permK. + by apply/mnmP=> k; rewrite !mnmE permKV. rewrite -(bij_eq bijF); have ->//: m#s#(s^-1)%g = m. by apply/mnmP=> k; rewrite !mnmE /= permKV. by close. 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