English
For a polynomial f, the open set imageOfDf equals the union of basic opens where some coefficient of f is nonzero; this set is open in Spec R.
Русский
Для многочлена f множество imageOfDf является объединением базовых открытых подмножеств, где какая-то коэффициент не равен нулю; множество открыто.
LaTeX
$$$\\text{imageOfDf}(f) = \\bigcup_{i \\in \\mathbb{N}} \\text{basicOpen}(f_i)$$$
Lean4
/-- Given a polynomial `f ∈ R[x]`, `imageOfDf` is the subset of `Spec R` where at least one
of the coefficients of `f` does not vanish. Lemma `imageOfDf_eq_comap_C_compl_zeroLocus`
proves that `imageOfDf` is the image of `(zeroLocus {f})ᶜ` under the morphism
`comap C : Spec R[x] → Spec R`. -/
def imageOfDf (f : R[X]) : Set (PrimeSpectrum R) :=
{p : PrimeSpectrum R | ∃ i : ℕ, coeff f i ∉ p.asIdeal}
