Theorem AlgebraicGeometry.Polynomial.comap_C_mem_imageOfDf

Modification history

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