Full ambient Hilbert dimension forces the ideal to be zero.
theorem
CCDN.ideal_eq_bot_of_full_hilbert_dimension
{K : Type u_1}
{σ : Type u_2}
[Field K]
[Fintype σ]
[LinearOrder σ]
(I : Ideal (MvPolynomial σ K))
(hI : I ≠ ⊤)
(hdim : (filteredHilbertPolynomial I).natDegree = Fintype.card σ)
:
A proper ideal whose filtered Hilbert polynomial has degree equal to the number of variables is the zero ideal.