feat: port AlgebraicGeometry.Morphisms.QuasiSeparated (#5691)

leanprover-community · Jul 4, 2023 · cc5d11f · cc5d11f
1 parent d57f6f3
commit cc5d11f
Show file tree

Hide file tree

Showing 2 changed files with 550 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -428,6 +428,7 @@ import Mathlib.AlgebraicGeometry.LocallyRingedSpace.HasColimits
 import Mathlib.AlgebraicGeometry.Morphisms.Basic
 import Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion
 import Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
+import Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
 import Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed
 import Mathlib.AlgebraicGeometry.OpenImmersion.Basic
 import Mathlib.AlgebraicGeometry.OpenImmersion.Scheme