Commit 2023-06-29 14:20 3c46000d

View on Github →

feat: port AlgebraicGeometry.Properties (#5585)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/AlgebraicGeometry/PrimeSpectrum/Basic.lean

Created Mathlib/AlgebraicGeometry/Properties.lean

added theorem AlgebraicGeometry.affine_isIntegral_iff

added theorem AlgebraicGeometry.affine_isReduced_iff

added theorem AlgebraicGeometry.basicOpen_eq_bot_iff

added theorem AlgebraicGeometry.eq_zero_of_basicOpen_eq_bot

added theorem AlgebraicGeometry.isIntegralOfIsAffineIsDomain

added theorem AlgebraicGeometry.isIntegralOfIsIrreducibleIsReduced

added theorem AlgebraicGeometry.isIntegralOfOpenImmersion

added theorem AlgebraicGeometry.isIntegral_iff_is_irreducible_and_isReduced

added theorem AlgebraicGeometry.isReducedOfIsAffineIsReduced

added theorem AlgebraicGeometry.isReducedOfOpenImmersion

added theorem AlgebraicGeometry.isReducedOfStalkIsReduced

added theorem AlgebraicGeometry.map_injective_of_isIntegral

added theorem AlgebraicGeometry.reduce_to_affine_global

added theorem AlgebraicGeometry.reduce_to_affine_nbhd