Commit 2025-01-20 16:09 8b8fcb5b

View on Github →

feat(AlgebraicGeometry): Instances regarding affine spaces (#20314)

Estimated changes

Modified Mathlib/AlgebraicGeometry/AffineSpace.lean

added theorem AlgebraicGeometry.AffineSpace.isIntegralHom_over_iff_isEmpty

added theorem AlgebraicGeometry.AffineSpace.isOpenMap_over

added theorem AlgebraicGeometry.AffineSpace.isPullback_map

added theorem AlgebraicGeometry.AffineSpace.map_toSpecMvPoly

added theorem AlgebraicGeometry.AffineSpace.not_isIntegralHom

modified def AlgebraicGeometry.AffineSpace.toSpecMvPoly

Modified Mathlib/AlgebraicGeometry/Limits.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/FinitePresentation.lean

deleted theorem AlgebraicGeometry.locallyOfFinitePresentation_isStableUnderBaseChange

Modified Mathlib/RingTheory/Spectrum/Prime/Polynomial.lean

added theorem MvPolynomial.comap_C_surjective

added theorem Polynomial.comap_C_surjective