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.image_of_Df_eq_comap_C_compl_zero_locus