Mathlib Changelog
v4
Changelog
About
Github
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