Mathlib v3 is deprecated. Go to Mathlib v4

Theorem algebraic_geometry.polynomial.comap_C_mem_image_of_Df

Modification history

2022-02-08 12:43
src/algebraic_geometry/prime_spectrum/is_open_comap_C.lean
feat(*): localized `R[X]` notation for `polynomial R` (#11895) …
Modified algebraic_geometry.polynomial.comap_C_mem_image_of_DfView on Github →
2021-01-20 09:51
src/algebraic_geometry/is_open_comap_C.lean
feat(algebraic_geometry/is_open_comap_C): add file is_open_comap_C, prove that Spec R[x] \to Spec R is an open map (#5693) …
Added algebraic_geometry.polynomial.comap_C_mem_image_of_DfView on Github →