Theorem AlgebraicGeometry.isField_of_universallyClosed

Modification history

2025-07-23 11:19
Mathlib/AlgebraicGeometry/Morphisms/Proper.lean
feat: `Spec(R)` notation for `Spec (CommRingCat.of R)` (#27031) …
Modified AlgebraicGeometry.isField_of_universallyClosedView on Github →
2025-02-15 17:47
Mathlib/AlgebraicGeometry/Morphisms/Proper.lean
feat(AlgebraicGeometry): Global sections of proper varieties (#21441)
Added AlgebraicGeometry.isField_of_universallyClosedView on Github →