mathlib

5f17f4da - feat(algebraic_geometry/prime_spectrum/basic): intersection of localisations (#16860)

feat(algebraic_geometry/prime_spectrum/basic): intersection of localisations (#16860) - [x] depends on: #16905 [define maximal spectrum] - [x] depends on: #16920 [refactor height one spectrum]