Theorem AlgebraicGeometry.Polynomial.imageOfDf_eq_comap_C_compl_zeroLocus

Modification history

2023-05-24 22:02
Mathlib/AlgebraicGeometry/PrimeSpectrum/IsOpenComapC.lean
feat: port AlgebraicGeometry.PrimeSpectrum.IsOpenComapC (#4302)
Added AlgebraicGeometry.Polynomial.imageOfDf_eq_comap_C_compl_zeroLocusView on Github →