Commit 2025-02-15 17:47 5395f521

View on Github →

feat(AlgebraicGeometry): Global sections of proper varieties (#21441)

Estimated changes

Modified Mathlib/AlgebraicGeometry/Morphisms/Proper.lean

added theorem AlgebraicGeometry.IsProper.of_comp_of_isSeparated

added theorem AlgebraicGeometry.UniversallyClosed.of_comp_of_isSeparated

added theorem AlgebraicGeometry.finite_appTop_of_universallyClosed

added theorem AlgebraicGeometry.isField_of_universallyClosed

added theorem AlgebraicGeometry.isIntegral_appTop_of_universallyClosed

Modified Mathlib/RingTheory/Jacobson/Ring.lean

added theorem finite_of_algHom_finiteType_of_isJacobsonRing