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