feat(Combinatorics/Nullstellensatz): formalize Alon's Combinatorial Nullstellensatz #20495
Conversation
AntoineChambert-Loir
removed
the
awaiting-author
mathlib4-dependent-issues-bot
added
the
blocked-by-other-PR
mathlib4-dependent-issues-bot
removed
the
blocked-by-other-PR
|
This PR/issue depends on: |
leanprover-community-bot-assistant
added
the
merge-conflict
github-actions
bot
removed
the
merge-conflict
| theorem eq_zero_of_eval_zero_at_prod_finset {σ : Type*} [Finite σ] [IsDomain R] | ||
| (P : MvPolynomial σ R) (S : σ → Finset R) | ||
| (Hdeg : ∀ i, P.degreeOf i < #(S i)) | ||
| (Heval : ∀ (x : σ → R), (∀ i, x i ∈ S i) → eval x P = 0) : | ||
| P = 0 := by |
There was a problem hiding this comment.
I suspect you would have a better time proving this one straight away using Finite.empty_option_induction and the Option version of MvPolynomial.finSuccEquiv (which already exists, but I can't give you the name because my computer is dead)
There was a problem hiding this comment.
I see your point, but unfortunately, docs#MvPolynomial.eval_eq_eval_mv_eval' is only for Fin n.succ. Let's see if I dare making the alternative version.
There was a problem hiding this comment.
Please have a look.
There was a problem hiding this comment.
I'm not completely happy with the optionEquivLeft_coeff_coeff, maybe it should incorporate what I do in the Nullstellensatz file. The point is that one needs, given m : sigma to0 Nat and d: Nat to construct an n : Option sigma to0 Nat, and the simplest way I found is adding single and embDomain....
YaelDillies
added
the
awaiting-author
Co-authored-by: Yaël Dillies <[email protected]>
AntoineChambert-Loir
removed
the
awaiting-author
Co-authored-by: Yaël Dillies <[email protected]>
This is a formalization of Alon's Combinatorial Nullstellensatz.
Meanwhile, prove several results
Probably, this file should belong to the
RingTheory.MvPolynomialhierarchy.