Commit 2024-11-19 11:44 f7b68aa4

View on Github →

feat(AlgebraicGeometry): ring hom is integral if the induced map between affine lines is closed (#18804)

Estimated changes

Modified Mathlib/Algebra/Polynomial/Reverse.lean

added theorem Polynomial.reflect_map

added theorem Polynomial.reflect_one

Modified Mathlib/AlgebraicGeometry/PrimeSpectrum/Basic.lean

added theorem PrimeSpectrum.closure_image_comap_zeroLocus

deleted theorem PrimeSpectrum.comap_singleton_isClosed_of_isIntegral

added theorem PrimeSpectrum.isClosedMap_comap_of_isIntegral

added theorem PrimeSpectrum.isClosed_comap_singleton_of_isIntegral

added theorem PrimeSpectrum.isIntegral_of_isClosedMap_comap_mapRingHom