Theorem AlgebraicGeometry.UniversallyClosed.of_comp_of_isSeparated

Modification history

2025-02-15 17:47
Mathlib/AlgebraicGeometry/Morphisms/Proper.lean
feat(AlgebraicGeometry): Global sections of proper varieties (#21441)
Added AlgebraicGeometry.UniversallyClosed.of_comp_of_isSeparatedView on Github →