Theorem AlgebraicGeometry.quasiSeparatedSpace_iff_quasiCompact_prod_lift

Modification history

2025-01-30 15:54
Mathlib/AlgebraicGeometry/Morphisms/QuasiSeparated.lean
feat(AlgebraicGeometry): `Π Rᵢ`-points of schemes (#20494)
Added AlgebraicGeometry.quasiSeparatedSpace_iff_quasiCompact_prod_liftView on Github →