Theorem AlgebraicGeometry.QuasiCompact.compactSpace_of_compactSpace

Modification history

2025-04-03 11:07
Mathlib/AlgebraicGeometry/Morphisms/QuasiCompact.lean
feat(AlgebraicGeometry): faithfully flat morphisms are topological quotient maps (#23608)
Added AlgebraicGeometry.QuasiCompact.compactSpace_of_compactSpaceView on Github →