Theorem AlgebraicGeometry.Scheme.IsOpenImmersion.of_isLocalization

Modification history

2024-08-02 19:53
Mathlib/AlgebraicGeometry/OpenImmersion.lean
feat(AlgebraicGeometry/Limits): Spec preserves finite coproducts (#14428)
Deleted AlgebraicGeometry.Scheme.IsOpenImmersion.of_isLocalizationView on Github →
2024-07-15 20:56
Mathlib/AlgebraicGeometry/OpenImmersion.lean
feat(AlgebraicGeometry/Limits): Coproducts of Schemes (#14429)
Added AlgebraicGeometry.Scheme.IsOpenImmersion.of_isLocalizationView on Github →