Theorem AlgebraicGeometry.IsIntegralHom.iff_universallyClosed_and_isAffineHom

Modification history

2025-02-04 06:00
Mathlib/AlgebraicGeometry/Morphisms/Integral.lean
feat(AlgebraicGeometry): integral = universally closed + affine (#19419) …
Added AlgebraicGeometry.IsIntegralHom.iff_universallyClosed_and_isAffineHomView on Github →