Commit 2025-04-06 21:05 4912cead

View on Github →

feat(Combinatorics/Nullstellensatz): Alon's combinatorial Nullstellensatz (#20495) This is a formalization of Alon's Combinatorial Nullstellensatz. Meanwhile, prove several results

a multivariate polynomial that vanishes on a too large product set vanishes identically Probably, this file should belong to the RingTheory.MvPolynomial hierarchy.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/MvPolynomial/Equiv.lean

modified theorem MvPolynomial.coeff_eval_eq_eval_coeff

added theorem MvPolynomial.optionEquivLeft_coeff_coeff

added theorem MvPolynomial.optionEquivLeft_elim_eval

added theorem MvPolynomial.optionEquivLeft_monomial

Created Mathlib/Combinatorics/Nullstellensatz.lean

added theorem MvPolynomial.combinatorial_nullstellensatz_exists_eval_nonzero

added theorem MvPolynomial.combinatorial_nullstellensatz_exists_linearCombination

added theorem MvPolynomial.eq_zero_of_eval_zero_at_prod_finset

Modified Mathlib/Data/Finsupp/Basic.lean

added theorem Finsupp.eq_option_embedding_update_none_iff

Modified Mathlib/RingTheory/MvPolynomial/Homogeneous.lean

added theorem MvPolynomial.weightedTotalDegree_rename_of_injective

Modified docs/references.bib