mathlib

d7e97106 - feat(ring_theory/polynomial/symmetric): restore `finset.powerset_len` version of `prod_X_sub_C_coeff` (#16424)

feat(ring_theory/polynomial/symmetric): restore `finset.powerset_len` version of `prod_X_sub_C_coeff` (#16424) In #15008, [`prod_X_add_C_coeff`](https://github.com/leanprover-community/mathlib/pull/15008/files#diff-08ead07a5e3b20f4db52e932b309a2ff767e486e4a0bf7d90b5520d25d95dc57L79-L81) was changed to use `multiset.esymm` in its RHS, which is defined in terms of `multiset.powerset_len` and not defeq to the original version which involves `finset.powerset_len` instead. This PR restores the `finset` version by introducing `finset.esymm_map_val`, a generalized version of `mv_polynomial.esymm_eq_multiset_esymm` (this lemma is renamed from `mv_polynomial.esymm_eq_multiset.esymm` to better conform with mathlib convention). Co-authored-by: negiizhao <egresf@gmail.com> [Zulip](https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Help.20with.20mv_polynomial/near/297702031) Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>