feat(Mathlib/Combinatorics/Nullstellensatz) : Alon's Combinatorial Nullstellensatz

[AntoineChambert-Loir]

Prove 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.

Question :

• The names Alon1 and Alon2 of the functions are not to stay, but I need suggestions.

---

• depends on: [Merged by Bors] - feat(Data/Finsupp/MonomialOrder): monomial orders #19453
• depends on: [Merged by Bors] - feat(RingTheory/MvPolynomial/Groebner): division algorithm wrt monomial orders #19454
• depends on: [Merged by Bors] - feat(Data/Finsupp/MonomialOrder/DegLex): homogeneous lexicographic order #19455

[github-actions]

PR summary 4d882612be

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.Data.Finsupp.MonomialOrder.DegLex (new file)	872
Mathlib.RingTheory.MvPolynomial.MonomialOrder (new file)	1102
Mathlib.RingTheory.MvPolynomial.Groebner (new file)	1103
Mathlib.RingTheory.MvPolynomial.MonomialOrder.DegLex (new file)	1105
Mathlib.Combinatorics.Nullstellensatz (new file)	1120

---

Declarations diff

+ Alon1
+ Alon2
+ DegLex.exists_iff
+ DegLex.forall_iff
+ DegLex.isStrictOrder
+ DegLex.le_iff
+ DegLex.linearOrder
+ DegLex.lt_def
+ DegLex.lt_iff
+ DegLex.monotone_degree
+ DegLex.orderBot
+ DegLex.partialOrder
+ DegLex.rec
+ DegLex.single_antitone
+ DegLex.single_le_iff
+ DegLex.single_lt_iff
+ DegLex.single_strictAnti
+ DegLex.wellFounded
+ DegLex.wellFoundedLT
+ Lex.single_antitone
+ Lex.single_le_iff
+ Lex.single_lt_iff
+ Lex.single_strictAnti
+ MonomialOrder.degLex
+ MonomialOrder.degLex_le_iff
+ MonomialOrder.degLex_lt_iff
+ MonomialOrder.degLex_single_le_iff
+ MonomialOrder.degLex_single_lt_iff
+ MonomialOrder.lex_unit_le_iff
+ MonomialOrder.lex_unit_lt_iff
+ _root_.MonomialOrder.degree_binomial
+ _root_.MonomialOrder.lCoeff_binomial
+ _root_.MonomialOrder.prod_degree
+ _root_.Polynomial.eq_zero_of_eval_zero
+ coeff_degree_eq_zero_iff
+ coeff_degree_ne_zero_iff
+ coeff_eq_zero_of_lt
+ coeff_mul_of_add_of_degree_le
+ coeff_mul_of_degree_add
+ coeff_prod_of_sum_degree
+ degLex_def
+ degLex_degree_degree
+ degLex_totalDegree_monotone
+ degree_C
+ degree_X
+ degree_X_le
+ degree_add
+ degree_add_le
+ degree_add_of_lt
+ degree_add_of_ne
+ degree_apply_single
+ degree_eq_zero_iff_totalDegree_eq_zero
+ degree_le_iff
+ degree_lt_iff
+ degree_monomial
+ degree_monomial_le
+ degree_mul
+ degree_mul_le
+ degree_mul_of_isRegular_left
+ degree_mul_of_isRegular_right
+ degree_mul_of_nonzero_mul
+ degree_neg
+ degree_of_not_nontrivial
+ degree_prod
+ degree_prod_le
+ degree_prod_of_regular
+ degree_reduce_lt
+ degree_single
+ degree_smul
+ degree_smul_le
+ degree_sub_LTerm_le
+ degree_sub_LTerm_lt
+ degree_sub_le
+ degree_sub_of_lt
+ div
+ div_set
+ eq_C_of_degree_eq_zero
+ eq_zero_of_eval_zero_at_prod
+ eq_zero_of_eval_zero_at_prod_nat
+ instance :
+ instance : OrderedCancelAddCommMonoid (DegLex (α →₀ ℕ))
+ instance [AddCommMonoid α] :
+ instance [LT α] : LT (DegLex (α →₀ ℕ))
+ lCoeff
+ lCoeff_add_of_lt
+ lCoeff_eq_zero_iff
+ lCoeff_is_unit_iff
+ lCoeff_monomial
+ lCoeff_mul
+ lCoeff_mul_of_isRegular_left
+ lCoeff_mul_of_isRegular_right
+ lCoeff_ne_zero_iff
+ lCoeff_of_not_nontrivial
+ lCoeff_prod_of_regular
+ lCoeff_sub_of_lt
+ lCoeff_zero
+ le_degree
+ ofDegLex
+ ofDegLex_add
+ ofDegLex_inj
+ ofDegLex_injective
+ ofDegLex_symm_eq
+ ofDegLex_toDegLex
+ reduce
+ subLTerm
+ sup_mem_of_nonempty
+ toDegLex
+ toDegLex_add
+ toDegLex_inj
+ toDegLex_injective
+ toDegLex_ofDegLex
+ toDegLex_symm_eq
+ weight_apply_single
+ weight_single_apply
+ weight_single_one_apply
+ weightedTotalDegree_rename_of_injective
++ DegLex
-++ degree
-++ degree_zero

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[github-actions]

Remaining comments which cannot be posted as a review comment to avoid GitHub Rate Limit

lint-style

---

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Line 381 in b2327b3

theorem eq_zero_of_eval_zero_at_prod_nat {n : ℕ} [IsDomain R]

---

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Lines 383 to 388 in b2327b3

	(Hdeg : ∀ i, P.weightedTotalDegree (Finsupp.single i 1) < (S i).ncard)
	(Heval : ∀ (x : Fin n → R), (∀ i, x i ∈ S i) → eval x P = 0) :
	P = 0 := by
	induction n generalizing R with
	| zero =>
	suffices P = C (constantCoeff P) by

---

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Line 392 in b2327b3

ext m

---

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Line 397 in b2327b3

| succ n hrec =>

---

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Line 399 in b2327b3

suffices Q = 0 by

---

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Lines 402 to 403 in b2327b3

	have Heval' : ∀ (x : Fin n → R) (_ : ∀ i, x i ∈ S i.succ),
	Polynomial.map (eval x) Q = 0 := fun x hx ↦ by

---

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Line 422 in b2327b3

· intro z _ hz

---

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Line 424 in b2327b3

· simp

---

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Line 428 in b2327b3

intro i

---

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Line 460 in b2327b3

noncomputable example (s : R) : Polynomial R := Polynomial.X (R := R) - Polynomial.C s

---

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Line 462 in b2327b3

noncomputable example (S : Finset R) : Polynomial R :=

---

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Line 476 in b2327b3

intro m hm

---

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Line 511 in b2327b3

rintro ⟨u, v⟩ h

---

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Lines 520 to 521 in b2327b3

	lemma prod_support_le {ι : Type*} (i : ι) (s : Finset R) (m : ι →₀ ℕ)
	(hm : m ∈ (s.prod (fun r ↦ X i - C r)).support) :

---

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Line 525 in b2327b3

| empty =>

---

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Line 532 in b2327b3

| @insert a s has h =>

---

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Line 607 in b2327b3

have hf : f = f' + monomial d (f.coeff d) := by

---

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Line 609 in b2327b3

have hf' : f'.support = f.support.erase d := by

---

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Line 623 in b2327b3

obtain ⟨h', r', Hf', Hh', Hr'⟩ := hrec f' hf'D

---

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Line 644 in b2327b3

rw [← ne_eq, ← mem_support_iff]

---

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Line 659 in b2327b3

-- write `monomial d (f.coeff d) = `monomial d' (f.coeff d) * _ + f''`

---

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Line 662 in b2327b3

have hf'' : monomial d (f.coeff d)

---

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Line 686 in b2327b3

by_cases h' : d' ≤ b

---

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Line 716 in b2327b3

simp only [Finset.mem_antidiagonal]

---

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Line 742 in b2327b3

obtain ⟨h'', r'', Hf'', Hh'', Hr''⟩ := hrec f'' hf''2

---

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Line 766 in b2327b3

· intro h

---

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Line 789 in b2327b3

· simp

---

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Line 796 in b2327b3

(f : MvPolynomial (Fin n) R) (Heval : ∀ (x : Fin n → R), (∀ i, x i ∈ S i) → eval x f = 0) :

---

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Line 803 in b2327b3

apply eq_zero_of_eval_zero_at_prod_nat r (fun i ↦ S i)

---

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Lines 818 to 822 in b2327b3

	theorem Alon2 {n : ℕ} [IsDomain R]
	(f : MvPolynomial (Fin n) R)
	(t : Fin n →₀ ℕ) (ht : f.coeff t ≠ 0) (ht' : f.totalDegree = t.degree)
	(S : Fin n → Finset R) (htS : ∀ i, t i < (S i).card) :
	∃ (s : Fin n → R) (_ : ∀ i, s i ∈ S i), eval s f ≠ 0 := by

---

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Lines 826 to 827 in b2327b3

	obtain ⟨h, hh, hf⟩ := Alon1 S
	(fun i ↦ by rw [← Finset.card_pos]; exact lt_of_le_of_lt (zero_le _) (htS i))

[github-actions]

Remaining comments which cannot be posted as a review comment to avoid GitHub Rate Limit

lint-style

---

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Line 386 in 244d91a

theorem eq_zero_of_eval_zero_at_prod_nat {n : ℕ} [IsDomain R]

---

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Lines 388 to 393 in 244d91a

	(Hdeg : ∀ i, P.weightedTotalDegree (Finsupp.single i 1) < (S i).ncard)
	(Heval : ∀ (x : Fin n → R), (∀ i, x i ∈ S i) → eval x P = 0) :
	P = 0 := by
	induction n generalizing R with
	| zero =>
	suffices P = C (constantCoeff P) by

---

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Line 397 in 244d91a

ext m

---

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Line 402 in 244d91a

| succ n hrec =>

---

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Line 404 in 244d91a

suffices Q = 0 by

---

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Lines 407 to 408 in 244d91a

	have Heval' : ∀ (x : Fin n → R) (_ : ∀ i, x i ∈ S i.succ),
	Polynomial.map (eval x) Q = 0 := fun x hx ↦ by

---

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Line 427 in 244d91a

· intro z _ hz

---

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Line 429 in 244d91a

· simp

---

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Line 433 in 244d91a

intro i

---

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Line 465 in 244d91a

noncomputable example (s : R) : Polynomial R := Polynomial.X (R := R) - Polynomial.C s

---

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Line 467 in 244d91a

noncomputable example (S : Finset R) : Polynomial R :=

---

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Line 481 in 244d91a

intro m hm

---

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Line 516 in 244d91a

rintro ⟨u, v⟩ h

---

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Lines 525 to 526 in 244d91a

	lemma prod_support_le {ι : Type*} (i : ι) (s : Finset R) (m : ι →₀ ℕ)
	(hm : m ∈ (s.prod (fun r ↦ X i - C r)).support) :

---

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Line 530 in 244d91a

| empty =>

---

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Line 537 in 244d91a

| @insert a s has h =>

---

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Line 612 in 244d91a

have hf : f = f' + monomial d (f.coeff d) := by

---

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Line 614 in 244d91a

have hf' : f'.support = f.support.erase d := by

---

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Line 628 in 244d91a

obtain ⟨h', r', Hf', Hh', Hr'⟩ := hrec f' hf'D

---

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Line 649 in 244d91a

rw [← ne_eq, ← mem_support_iff]

---

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Line 664 in 244d91a

-- write `monomial d (f.coeff d) = `monomial d' (f.coeff d) * _ + f''`

---

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Line 667 in 244d91a

have hf'' : monomial d (f.coeff d)

---

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Line 691 in 244d91a

by_cases h' : d' ≤ b

---

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Line 721 in 244d91a

simp only [Finset.mem_antidiagonal]

---

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Line 747 in 244d91a

obtain ⟨h'', r'', Hf'', Hh'', Hr''⟩ := hrec f'' hf''2

---

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Line 771 in 244d91a

· intro h

---

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Line 794 in 244d91a

· simp

---

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Line 801 in 244d91a

(f : MvPolynomial (Fin n) R) (Heval : ∀ (x : Fin n → R), (∀ i, x i ∈ S i) → eval x f = 0) :

---

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Line 808 in 244d91a

apply eq_zero_of_eval_zero_at_prod_nat r (fun i ↦ S i)

---

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Lines 823 to 827 in 244d91a

	theorem Alon2 {n : ℕ} [IsDomain R]
	(f : MvPolynomial (Fin n) R)
	(t : Fin n →₀ ℕ) (ht : f.coeff t ≠ 0) (ht' : f.totalDegree = t.degree)
	(S : Fin n → Finset R) (htS : ∀ i, t i < (S i).card) :
	∃ (s : Fin n → R) (_ : ∀ i, s i ∈ S i), eval s f ≠ 0 := by

---

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Lines 831 to 832 in 244d91a

	obtain ⟨h, hh, hf⟩ := Alon1 S
	(fun i ↦ by rw [← Finset.card_pos]; exact lt_of_le_of_lt (zero_le _) (htS i))

[github-actions]

Remaining comments which cannot be posted as a review comment to avoid GitHub Rate Limit

lint-style

---

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Line 832 in 74b2d05

· simp

---

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Line 839 in 74b2d05

/- theorem euclDivd {n : ℕ} (S : Fin n → Finset R) (Sne : ∀ i, (S i).Nonempty)

---

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Line 866 in 74b2d05

have hf : f = f' + monomial d (f.coeff d) := by

---

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Line 868 in 74b2d05

have hf' : f'.support = f.support.erase d := by

---

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Line 882 in 74b2d05

obtain ⟨h', r', Hf', Hh', Hr'⟩ := hrec f' hf'D

---

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Line 903 in 74b2d05

rw [← ne_eq, ← mem_support_iff]

---

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Line 918 in 74b2d05

-- write `monomial d (f.coeff d) = `monomial d' (f.coeff d) * _ + f''`

---

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Line 921 in 74b2d05

have hf'' : monomial d (f.coeff d)

---

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Line 945 in 74b2d05

by_cases h' : d' ≤ b

---

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Line 975 in 74b2d05

simp only [Finset.mem_antidiagonal]

---

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Line 1001 in 74b2d05

obtain ⟨h'', r'', Hf'', Hh'', Hr''⟩ := hrec f'' hf''2

---

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Line 1025 in 74b2d05

· intro h

---

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Line 1048 in 74b2d05

· simp

---

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Line 1056 in 74b2d05

(f : MvPolynomial σ R) (Heval : ∀ (x : σ → R), (∀ i, x i ∈ S i) → eval x f = 0) :

---

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Line 1063 in 74b2d05

apply eq_zero_of_eval_zero_at_prod r (fun i ↦ S i)

---

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Lines 1078 to 1082 in 74b2d05

	theorem Alon2 [IsDomain R]
	(f : MvPolynomial σ R)
	(t : σ →₀ ℕ) (ht : f.coeff t ≠ 0) (ht' : f.totalDegree = t.degree)
	(S : σ → Finset R) (htS : ∀ i, t i < (S i).card) :
	∃ (s : σ → R) (_ : ∀ i, s i ∈ S i), eval s f ≠ 0 := by

---

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Lines 1087 to 1088 in 74b2d05

	obtain ⟨h, hh, hf⟩ := Alon1 S
	(fun i ↦ by rw [← Finset.card_pos]; exact lt_of_le_of_lt (zero_le _) (htS i))

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• [Merged by Bors] - feat(Data/Finsupp/MonomialOrder): monomial orders #19453
• [Merged by Bors] - feat(RingTheory/MvPolynomial/Groebner): division algorithm wrt monomial orders #19454
• [Merged by Bors] - feat(Data/Finsupp/MonomialOrder/DegLex): homogeneous lexicographic order #19455
  By Dependent Issues (🤖). Happy coding!