# Commit 2022-09-19 15:19 d7e97106

View on Github →feat(ring_theory/polynomial/symmetric): restore `finset.powerset_len`

version of `prod_X_sub_C_coeff`

(#16424)
In #15008, `prod_X_add_C_coeff`

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).
Zulip