Mathlib v3 is deprecated. Go to Mathlib v4

Theorem algebraic_geometry.quasi_separated_eq_diagonal_is_quasi_compact

Modification history

2022-10-24 07:29

src/algebraic_geometry/morphisms/quasi_separated.lean

feat(src/algebraic_geometry/morphisms/quasi_separated): Define quasi-separated morphisms. (#17080)

Added algebraic_geometry.quasi_separated_eq_diagonal_is_quasi_compact View on Github →