mathlib3

a7a4f34c - 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)

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) This file is the first part of a proof of Chevalley's Theorem. It contains a proof that the morphism Spec R[x] \to Spec R is open. In a later PR, I hope to prove that, under the same morphism, the image of a closed set is constructible.