Commit 2023-05-24 22:02 52d71ad9

View on Github →

feat: port AlgebraicGeometry.PrimeSpectrum.IsOpenComapC (#4302)

Estimated changes

Modified Mathlib.lean

Created Mathlib/AlgebraicGeometry/PrimeSpectrum/IsOpenComapC.lean

added theorem AlgebraicGeometry.Polynomial.comap_C_mem_imageOfDf

added def AlgebraicGeometry.Polynomial.imageOfDf

added theorem AlgebraicGeometry.Polynomial.imageOfDf_eq_comap_C_compl_zeroLocus

added theorem AlgebraicGeometry.Polynomial.isOpenMap_comap_c

added theorem AlgebraicGeometry.Polynomial.isOpen_imageOfDf