Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-12-01 08:15 94625350

View on Github →

feat(algebraic_geometry): Qcqs lemma (#15996)

Estimated changes

Modified docs/references.bib

Modified src/algebraic_geometry/AffineScheme.lean

Modified src/algebraic_geometry/morphisms/quasi_compact.lean

added theorem algebraic_geometry.exists_pow_mul_eq_zero_of_res_basic_open_eq_zero_of_is_affine_open

added theorem algebraic_geometry.exists_pow_mul_eq_zero_of_res_basic_open_eq_zero_of_is_compact

Modified src/algebraic_geometry/morphisms/quasi_separated.lean

added theorem algebraic_geometry.exists_eq_pow_mul_of_is_affine_open

added theorem algebraic_geometry.exists_eq_pow_mul_of_is_compact_of_is_quasi_separated

added theorem algebraic_geometry.exists_eq_pow_mul_of_is_compact_of_quasi_separated_space_aux

added theorem algebraic_geometry.is_localization_basic_open_of_qcqs