Theorem AlgebraicGeometry.IsOpenImmersion.image_preimage_eq_preimage_image_of_isPullback

Modification history

2025-02-12 14:43
Mathlib/AlgebraicGeometry/OpenImmersion.lean
feat(AlgebraicGeometry): the kernel of a morphism (#21431)
Added AlgebraicGeometry.IsOpenImmersion.image_preimage_eq_preimage_image_of_isPullbackView on Github →