theorem CommutativeAlgebra.hilbert_nullstellensatz_base (n : ℕ) (I : Ideal (MvPolynomial (Fin n) ℂ)) : I.IsMaximal ↔ ∃ (a : Fin n → ℂ), I = MvPolynomial.vanishingIdeal ℂ {a}

theorem CommutativeAlgebra.vanishingIdeal_singleton_eq_ker_aeval (n : ℕ) (a : Fin n → ℂ) : MvPolynomial.vanishingIdeal ℂ {a} = RingHom.ker (MvPolynomial.aeval a)

theorem CommutativeAlgebra.hilbert_nullstellensatz_weak_ker (n : ℕ) (I : Ideal (MvPolynomial (Fin n) ℂ)) : I.IsMaximal ↔ ∃ (a : Fin n → ℂ), I = RingHom.ker (MvPolynomial.aeval a)

theorem CommutativeAlgebra.hilbert_nullstellensatz_weak (n m : ℕ) (P : Fin m → MvPolynomial (Fin n) ℂ) (J : Ideal (MvPolynomial (Fin n) ℂ ⧸ Ideal.span (Set.range P))) : J.IsMaximal ↔ ∃ (a : Fin n → ℂ), (∀ (i : Fin m), (MvPolynomial.aeval a) (P i) = 0) ∧ J = Ideal.map (Ideal.Quotient.mk (Ideal.span (Set.range P))) (MvPolynomial.vanishingIdeal ℂ {a})