mathlib

bd578040 - feat(algebraic_geometry/prime_spectrum): add lemma zero_locus_bUnion (#5692)

feat(algebraic_geometry/prime_spectrum): add lemma zero_locus_bUnion (#5692) Add a simple extension of a lemma, to be able to work with `bUnion`, instead of only `Union`. Co-authored-by: Johan Commelin <johan@commelin.net>