mathlib

6fa3fc3e - feat(algebraic_geometry/prime_spectrum/basic): new lemmas + golf (#17289)

feat(algebraic_geometry/prime_spectrum/basic): new lemmas + golf (#17289) Extract lemmas `closure_singleton`, `is_radical_vanishing_ideal`, and `is_irreducible_iff_vanishing_ideal_is_prime` to golf `prime_spectrum.quasi_sober`; also add a convenient but unused lemma `vanishing_ideal_eq_top_iff`. - [x] depends on: #17254 Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>