From 15a3b8713863634c64d3b84a6c58e895241ddc23 Mon Sep 17 00:00:00 2001 From: Andrew Yang Date: Thu, 24 Oct 2024 03:32:15 +0100 Subject: [PATCH] Update Mathlib.lean --- Mathlib.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/Mathlib.lean b/Mathlib.lean index e9a3b499c9093..84795a58c9663 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -877,6 +877,7 @@ import Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion import Mathlib.AlgebraicGeometry.Morphisms.Constructors import Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation import Mathlib.AlgebraicGeometry.Morphisms.FiniteType +import Mathlib.AlgebraicGeometry.Morphisms.Immersion import Mathlib.AlgebraicGeometry.Morphisms.IsIso import Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion import Mathlib.AlgebraicGeometry.Morphisms.Preimmersion