Mathlib v3 is deprecated. Go to Mathlib v4

Theorem algebraic_geometry.polynomial.is_open_image_of_Df

Modification history

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.is_open_image_of_DfView on Github →