Commit 2022-09-19 15:19 d7e97106

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