mathlib3
4d19f5fa - feat(algebraic_geometry): Basic opens form basis of zariski topology (#7152)

Commit

4 years ago

feat(algebraic_geometry): Basic opens form basis of zariski topology (#7152) Fills in a few lemmas in `prime_spectrum.lean`, in particular that basic opens form a basis

Author

justus-springer

Parents

724f804b

mathlib3 4d19f5fa - feat(algebraic_geometry): Basic opens form basis of zariski topology (#7152)

mathlib3
4d19f5fa - feat(algebraic_geometry): Basic opens form basis of zariski topology (#7152)