feat: port AlgebraicGeometry.ProjectiveSpectrum.Topology (#4171)

leanprover-community · May 21, 2023 · 92b28a1 · 92b28a1
1 parent a1ec399
commit 92b28a1
Show file tree

Hide file tree

Showing 2 changed files with 508 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -334,6 +334,7 @@ import Mathlib.Algebra.Tropical.Basic
 import Mathlib.Algebra.Tropical.BigOperators
 import Mathlib.Algebra.Tropical.Lattice
 import Mathlib.AlgebraicGeometry.PresheafedSpace
+import Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
 import Mathlib.AlgebraicTopology.AlternatingFaceMapComplex
 import Mathlib.AlgebraicTopology.CechNerve
 import Mathlib.AlgebraicTopology.DoldKan.Compatibility