mathlib3

feat(algebraic_geometry) : closed immersion

#14899

Open