Commit 2025-10-06 20:40 900513ac

View on Github →

feat(AlgebraicGeometry): quasi-affine schemes (#30256)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/OpenImmersion.lean

added theorem AlgebraicGeometry.IsOpenImmersion.of_forall_source_exists

added theorem AlgebraicGeometry.IsOpenImmersion.of_openCover_source

Modified Mathlib/AlgebraicGeometry/Morphisms/QuasiSeparated.lean

deleted theorem AlgebraicGeometry.isIso_ΓSpec_adjunction_unit_app_basicOpen

Modified Mathlib/AlgebraicGeometry/Morphisms/Separated.lean

Created Mathlib/AlgebraicGeometry/QuasiAffine.lean

added theorem AlgebraicGeometry.Scheme.IsQuasiAffine.of_isImmersion