Theorems · Definition · algebraic geometry

PrimeSpectrum.BasicConstructibleSetData.toSet

{R : Type u_1} → [inst : CommSemiring R] → PrimeSpectrum.BasicConstructibleSetData R → Set (PrimeSpectrum R)

Given the data of a basic constructible set s, namely a tuple (f, g₁, ..., gₙ) such that s = V(g₁, ..., gₙ) \ V(f), return s.

Defined in

Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet

Cited by

4 results in Mathlib

Foundations

Depth 17 from the axioms · uses no axioms

Assumes

CommSemiring