The zero locus of an ideal of multivariate polynomials, with coordinates in the
coefficient ring. Over a field K this is Mathlib's MvPolynomial.zeroLocus K I,
stated with eval rather than aeval; that definition is reserved for points with
coordinates in an extension field.
def
CCDN.idealZeroLocus
{K : Type u_1}
{σ : Type u_2}
[CommRing K]
(I : Ideal (MvPolynomial σ K))
:
Set (σ → K)
The common zeros, with coordinates in the coefficient ring, of all polynomials in I.
Equations
- CCDN.idealZeroLocus I = {x : σ → K | ∀ f ∈ I, (MvPolynomial.eval x) f = 0}