Using Mathlib's Combinatorial Nullstellensatz: top coefficient via Vieta + homogeneity

To apply MvPolynomial.combinatorial_nullstellensatz_exists_eval_nonzero (needs f.coeff t ≠ 0 and f.totalDegree = t.degree) to a polynomial like (x-y)∏_{c∈C}(x+y-c) over Fin 2, do not expand the product. (1) Push Multiset.prod_X_add_C_eq_sum_esymm (C.val.map Neg.neg) through Polynomial.aeval (X 0 + X 1) to get ∑_j C(e_j) (x+y)^{|C|-j}. (2) Terms with j>0 are IsHomogeneous of smaller degree (build with isHomogeneous_X, .sub, .add, .pow, .mul), so IsHomogeneous.coeff_eq_zero kills them; Multiset.esymm_zero handles j=0. (3) For totalDegree, get ≤ from totalDegree_mul + totalDegree_finsetProd + totalDegree_sub_C_le, and ≥ from le_totalDegree (mem_support_iff.2 hne). (4) Get coefficients of (x+y)^m at single 0 i + single 1 j from add_pow, X_pow_eq_monomial, monomial_mul_monomial, C_mul_monomial, coeff_monomial; peel a linear factor with coeff_X_mul : (X s * p).coeff (single s 1 + m) = p.coeff m. Gotchas in Mathlib 2026: root if_pos/if_neg are deprecated (use ite_eq_left/ite_eq_right); Field (ZMod p) needs Mathlib.Algebra.Field.ZMod; linear_combination needs Mathlib.Tactic.LinearCombination in module files.