chore(algebraic_geometry/prime_spectrum/basic): remove TODO (#12768)

Sober topological spaces has been defined and it has been proven (in this file) that prime spectrum is sober
leanprover-community · Mar 18, 2022 · 241d63d · 241d63d
1 parent cfa7f6a
commit 241d63d
Showing 1 changed file with 0 additions and 2 deletions.
diff --git a/src/algebraic_geometry/prime_spectrum/basic.lean b/src/algebraic_geometry/prime_spectrum/basic.lean
@@ -718,8 +718,6 @@ section order
 
 We endow `prime_spectrum R` with a partial order,
 where `x ≤ y` if and only if `y ∈ closure {x}`.
-
-TODO: maybe define sober topological spaces, and generalise this instance to those
 -/
 
 instance : partial_order (prime_spectrum R) :=