feat: port AlgebraicTopology.CechNerve (#3500)

leanprover-community · Apr 19, 2023 · 9db4c68 · 9db4c68
1 parent 96f9551
commit 9db4c68
Show file tree

Hide file tree

Showing 3 changed files with 452 additions and 2 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -292,6 +292,7 @@ import Mathlib.Algebra.TrivSqZeroExt
 import Mathlib.Algebra.Tropical.Basic
 import Mathlib.Algebra.Tropical.BigOperators
 import Mathlib.Algebra.Tropical.Lattice
+import Mathlib.AlgebraicTopology.CechNerve
 import Mathlib.AlgebraicTopology.DoldKan.Compatibility
 import Mathlib.AlgebraicTopology.MooreComplex
 import Mathlib.AlgebraicTopology.SimplexCategory