mathlib

a6f325fe - feat(algebraic_geometry): comap of surjective homomorphism is closed embedding (#15291)

feat(algebraic_geometry): comap of surjective homomorphism is closed embedding (#15291) The comap of a surjective homomorphism is a closed embedding between the Zariski spectra. Co-authored-by: Jake Levinson @jakelev Co-authored-by: Jake Levinson <levinson.jake@gmail.com>