Commit 2024-12-23 15:20 cd2213b6

View on Github →

feat(AlgebraicGeometry): Spec R[X] -> Spec R is open (#20159)

Estimated changes

Modified Mathlib.lean

Created Mathlib/AlgebraicGeometry/PrimeSpectrum/Polynomial.lean

added theorem MvPolynomial.image_comap_C_basicOpen

added theorem MvPolynomial.isOpenMap_comap_C

added theorem MvPolynomial.mem_image_comap_C_basicOpen

added theorem Polynomial.exists_image_comap_of_monic

added theorem Polynomial.image_comap_C_basicOpen

added theorem Polynomial.isCompact_image_comap_of_monic

added theorem Polynomial.isOpenMap_comap_C

added theorem Polynomial.isOpen_image_comap_of_monic

added theorem Polynomial.mem_image_comap_C_basicOpen

added theorem PrimeSpectrum.exists_image_comap_of_finite_of_free

added theorem PrimeSpectrum.mem_image_comap_basicOpen

added theorem PrimeSpectrum.mem_image_comap_zeroLocus_sdiff

added theorem isNilpotent_tensor_residueField_iff

Modified Mathlib/RingTheory/TensorProduct/MvPolynomial.lean

added theorem MvPolynomial.rTensorAlgEquiv_apply