Theorems · Definition · algebraic geometry

PrimeSpectrum.ConstructibleSetData.toSet

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

Given the data of a constructible set s, namely finitely many tuples (f, g₁, ..., gₙ) such that s = ⋃ (f, g₁, ..., gₙ), V(g₁, ..., gₙ) \ V(f), return s.

Defined in

Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet

Cited by

8 results in Mathlib

Foundations

Depth 54 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommSemiring