Theorem AlgebraicGeometry.IsLocalIso.eq_sourceLocalClosure_isOpenImmersion

Modification history

2025-07-23 10:07
Mathlib/AlgebraicGeometry/Morphisms/LocalIso.lean
feat(AlgebraicGeometry): source-local closure of a morphism property (#26723) …
Added AlgebraicGeometry.IsLocalIso.eq_sourceLocalClosure_isOpenImmersionView on Github →