Theorem AlgebraicGeometry.Scheme.AffineZariskiSite.PreservesLocalization.isOpenImmersion

Modification history

2026-08-31 13:50

Mathlib/AlgebraicGeometry/Sites/SmallAffineZariski.lean

chore: delete deprecated declarations from February 2026 (#43178) …

Deleted AlgebraicGeometry.Scheme.AffineZariskiSite.PreservesLocalization.isOpenImmersion View on Github →

2025-12-09 18:53

Mathlib/AlgebraicGeometry/Sites/SmallAffineZariski.lean

feat(AlgebraicGeometry): "quasi-coherent `𝒪ₓ`-algebras" (#32595)

Added AlgebraicGeometry.Scheme.AffineZariskiSite.PreservesLocalization.isOpenImmersion View on Github →